Runtime Complexity (innermost) proof of /tmp/tmp2X3bHn/Ex26_Luc03b

The Runtime Complexity (innermost) of the given CpxTRS could be proven to be BOUNDS(1, n^1).

0 CpxTRS

↳1 TrsToWeightedTrsProof (BOTH BOUNDS(ID, ID), 0 ms)

↳2 CpxWeightedTrs

↳3 InnermostUnusableRulesProof (BOTH BOUNDS(ID, ID), 0 ms)

↳4 CpxWeightedTrs

↳5 TypeInferenceProof (BOTH BOUNDS(ID, ID), 5 ms)

↳6 CpxTypedWeightedTrs

↳7 CompletionProof (UPPER BOUND(ID), 0 ms)

↳8 CpxTypedWeightedCompleteTrs

↳9 NarrowingProof (BOTH BOUNDS(ID, ID), 0 ms)

↳10 CpxTypedWeightedCompleteTrs

↳11 CpxTypedWeightedTrsToRntsProof (UPPER BOUND(ID), 6 ms)

↳12 CpxRNTS

↳13 InliningProof (UPPER BOUND(ID), 282 ms)

↳14 CpxRNTS

↳15 SimplificationProof (BOTH BOUNDS(ID, ID), 0 ms)

↳16 CpxRNTS

↳17 CpxRntsAnalysisOrderProof (BOTH BOUNDS(ID, ID), 6 ms)

↳18 CpxRNTS

↳19 IntTrsBoundProof (UPPER BOUND(ID), 354 ms)

↳20 CpxRNTS

↳21 IntTrsBoundProof (UPPER BOUND(ID), 10 ms)

↳22 CpxRNTS

↳23 ResultPropagationProof (UPPER BOUND(ID), 0 ms)

↳24 CpxRNTS

↳25 IntTrsBoundProof (UPPER BOUND(ID), 97 ms)

↳26 CpxRNTS

↳27 IntTrsBoundProof (UPPER BOUND(ID), 5 ms)

↳28 CpxRNTS

↳29 ResultPropagationProof (UPPER BOUND(ID), 0 ms)

↳30 CpxRNTS

↳31 IntTrsBoundProof (UPPER BOUND(ID), 270 ms)

↳32 CpxRNTS

↳33 IntTrsBoundProof (UPPER BOUND(ID), 6 ms)

↳34 CpxRNTS

↳35 ResultPropagationProof (UPPER BOUND(ID), 0 ms)

↳36 CpxRNTS

↳37 IntTrsBoundProof (UPPER BOUND(ID), 166 ms)

↳38 CpxRNTS

↳39 IntTrsBoundProof (UPPER BOUND(ID), 67 ms)

↳40 CpxRNTS

↳41 ResultPropagationProof (UPPER BOUND(ID), 0 ms)

↳42 CpxRNTS

↳43 IntTrsBoundProof (UPPER BOUND(ID), 126 ms)

↳44 CpxRNTS

↳45 IntTrsBoundProof (UPPER BOUND(ID), 8 ms)

↳46 CpxRNTS

↳47 ResultPropagationProof (UPPER BOUND(ID), 0 ms)

↳48 CpxRNTS

↳49 IntTrsBoundProof (UPPER BOUND(ID), 150 ms)

↳50 CpxRNTS

↳51 IntTrsBoundProof (UPPER BOUND(ID), 22 ms)

↳52 CpxRNTS

↳53 ResultPropagationProof (UPPER BOUND(ID), 1 ms)

↳54 CpxRNTS

↳55 IntTrsBoundProof (UPPER BOUND(ID), 7310 ms)

↳56 CpxRNTS

↳57 IntTrsBoundProof (UPPER BOUND(ID), 750 ms)

↳58 CpxRNTS

↳59 FinalProof (⇔, 0 ms)

↳60 BOUNDS(1, n^1)

(0) Obligation:

The Runtime Complexity (innermost) of the given CpxTRS could be proven to be BOUNDS(1, n^1).

The TRS R consists of the following rules:

terms(N) → cons(recip(sqr(N)), n__terms(n__s(N)))
sqr(0) → 0
sqr(s(X)) → s(n__add(n__sqr(activate(X)), n__dbl(activate(X))))
dbl(0) → 0
dbl(s(X)) → s(n__s(n__dbl(activate(X))))
add(0, X) → X
add(s(X), Y) → s(n__add(activate(X), Y))
first(0, X) → nil
first(s(X), cons(Y, Z)) → cons(Y, n__first(activate(X), activate(Z)))
terms(X) → n__terms(X)
s(X) → n__s(X)
add(X1, X2) → n__add(X1, X2)
sqr(X) → n__sqr(X)
dbl(X) → n__dbl(X)
first(X1, X2) → n__first(X1, X2)
activate(n__terms(X)) → terms(activate(X))
activate(n__s(X)) → s(X)
activate(n__add(X1, X2)) → add(activate(X1), activate(X2))
activate(n__sqr(X)) → sqr(activate(X))
activate(n__dbl(X)) → dbl(activate(X))
activate(n__first(X1, X2)) → first(activate(X1), activate(X2))
activate(X) → X

Rewrite Strategy: INNERMOST

(1) TrsToWeightedTrsProof (BOTH BOUNDS(ID, ID) transformation)

Transformed TRS to weighted TRS

(2) Obligation:

The Runtime Complexity (innermost) of the given CpxWeightedTrs could be proven to be BOUNDS(1, n^1).

The TRS R consists of the following rules:

terms(N) → cons(recip(sqr(N)), n__terms(n__s(N))) [1]
sqr(0) → 0 [1]
sqr(s(X)) → s(n__add(n__sqr(activate(X)), n__dbl(activate(X)))) [1]
dbl(0) → 0 [1]
dbl(s(X)) → s(n__s(n__dbl(activate(X)))) [1]
add(0, X) → X [1]
add(s(X), Y) → s(n__add(activate(X), Y)) [1]
first(0, X) → nil [1]
first(s(X), cons(Y, Z)) → cons(Y, n__first(activate(X), activate(Z))) [1]
terms(X) → n__terms(X) [1]
s(X) → n__s(X) [1]
add(X1, X2) → n__add(X1, X2) [1]
sqr(X) → n__sqr(X) [1]
dbl(X) → n__dbl(X) [1]
first(X1, X2) → n__first(X1, X2) [1]
activate(n__terms(X)) → terms(activate(X)) [1]
activate(n__s(X)) → s(X) [1]
activate(n__add(X1, X2)) → add(activate(X1), activate(X2)) [1]
activate(n__sqr(X)) → sqr(activate(X)) [1]
activate(n__dbl(X)) → dbl(activate(X)) [1]
activate(n__first(X1, X2)) → first(activate(X1), activate(X2)) [1]
activate(X) → X [1]

Rewrite Strategy: INNERMOST

(3) InnermostUnusableRulesProof (BOTH BOUNDS(ID, ID) transformation)

Removed the following rules with non-basic left-hand side, as they cannot be used in innermost rewriting:

sqr(s(X)) → s(n__add(n__sqr(activate(X)), n__dbl(activate(X)))) [1]
dbl(s(X)) → s(n__s(n__dbl(activate(X)))) [1]
add(s(X), Y) → s(n__add(activate(X), Y)) [1]
first(s(X), cons(Y, Z)) → cons(Y, n__first(activate(X), activate(Z))) [1]

Due to the following rules that have to be used instead:

s(X) → n__s(X) [1]

(4) Obligation:

The Runtime Complexity (innermost) of the given CpxWeightedTrs could be proven to be BOUNDS(1, n^1).

The TRS R consists of the following rules:

terms(N) → cons(recip(sqr(N)), n__terms(n__s(N))) [1]
sqr(0) → 0 [1]
dbl(0) → 0 [1]
add(0, X) → X [1]
first(0, X) → nil [1]
terms(X) → n__terms(X) [1]
s(X) → n__s(X) [1]
add(X1, X2) → n__add(X1, X2) [1]
sqr(X) → n__sqr(X) [1]
dbl(X) → n__dbl(X) [1]
first(X1, X2) → n__first(X1, X2) [1]
activate(n__terms(X)) → terms(activate(X)) [1]
activate(n__s(X)) → s(X) [1]
activate(n__add(X1, X2)) → add(activate(X1), activate(X2)) [1]
activate(n__sqr(X)) → sqr(activate(X)) [1]
activate(n__dbl(X)) → dbl(activate(X)) [1]
activate(n__first(X1, X2)) → first(activate(X1), activate(X2)) [1]
activate(X) → X [1]

Rewrite Strategy: INNERMOST

(5) TypeInferenceProof (BOTH BOUNDS(ID, ID) transformation)

Infered types.

(6) Obligation:

Runtime Complexity Weighted TRS with Types.
The TRS R consists of the following rules:

terms(N) → cons(recip(sqr(N)), n__terms(n__s(N))) [1]
sqr(0) → 0 [1]
dbl(0) → 0 [1]
add(0, X) → X [1]
first(0, X) → nil [1]
terms(X) → n__terms(X) [1]
s(X) → n__s(X) [1]
add(X1, X2) → n__add(X1, X2) [1]
sqr(X) → n__sqr(X) [1]
dbl(X) → n__dbl(X) [1]
first(X1, X2) → n__first(X1, X2) [1]
activate(n__terms(X)) → terms(activate(X)) [1]
activate(n__s(X)) → s(X) [1]
activate(n__add(X1, X2)) → add(activate(X1), activate(X2)) [1]
activate(n__sqr(X)) → sqr(activate(X)) [1]
activate(n__dbl(X)) → dbl(activate(X)) [1]
activate(n__first(X1, X2)) → first(activate(X1), activate(X2)) [1]
activate(X) → X [1]

The TRS has the following type information:

terms :: n__s:n__terms:cons:0:nil:n__add:n__sqr:n__dbl:n__first → n__s:n__terms:cons:0:nil:n__add:n__sqr:n__dbl:n__first
cons :: recip → n__s:n__terms:cons:0:nil:n__add:n__sqr:n__dbl:n__first → n__s:n__terms:cons:0:nil:n__add:n__sqr:n__dbl:n__first
recip :: n__s:n__terms:cons:0:nil:n__add:n__sqr:n__dbl:n__first → recip
sqr :: n__s:n__terms:cons:0:nil:n__add:n__sqr:n__dbl:n__first → n__s:n__terms:cons:0:nil:n__add:n__sqr:n__dbl:n__first
n__terms :: n__s:n__terms:cons:0:nil:n__add:n__sqr:n__dbl:n__first → n__s:n__terms:cons:0:nil:n__add:n__sqr:n__dbl:n__first
n__s :: n__s:n__terms:cons:0:nil:n__add:n__sqr:n__dbl:n__first → n__s:n__terms:cons:0:nil:n__add:n__sqr:n__dbl:n__first
0 :: n__s:n__terms:cons:0:nil:n__add:n__sqr:n__dbl:n__first
dbl :: n__s:n__terms:cons:0:nil:n__add:n__sqr:n__dbl:n__first → n__s:n__terms:cons:0:nil:n__add:n__sqr:n__dbl:n__first
add :: n__s:n__terms:cons:0:nil:n__add:n__sqr:n__dbl:n__first → n__s:n__terms:cons:0:nil:n__add:n__sqr:n__dbl:n__first → n__s:n__terms:cons:0:nil:n__add:n__sqr:n__dbl:n__first
first :: n__s:n__terms:cons:0:nil:n__add:n__sqr:n__dbl:n__first → n__s:n__terms:cons:0:nil:n__add:n__sqr:n__dbl:n__first → n__s:n__terms:cons:0:nil:n__add:n__sqr:n__dbl:n__first
nil :: n__s:n__terms:cons:0:nil:n__add:n__sqr:n__dbl:n__first
s :: n__s:n__terms:cons:0:nil:n__add:n__sqr:n__dbl:n__first → n__s:n__terms:cons:0:nil:n__add:n__sqr:n__dbl:n__first
n__add :: n__s:n__terms:cons:0:nil:n__add:n__sqr:n__dbl:n__first → n__s:n__terms:cons:0:nil:n__add:n__sqr:n__dbl:n__first → n__s:n__terms:cons:0:nil:n__add:n__sqr:n__dbl:n__first
n__sqr :: n__s:n__terms:cons:0:nil:n__add:n__sqr:n__dbl:n__first → n__s:n__terms:cons:0:nil:n__add:n__sqr:n__dbl:n__first
n__dbl :: n__s:n__terms:cons:0:nil:n__add:n__sqr:n__dbl:n__first → n__s:n__terms:cons:0:nil:n__add:n__sqr:n__dbl:n__first
n__first :: n__s:n__terms:cons:0:nil:n__add:n__sqr:n__dbl:n__first → n__s:n__terms:cons:0:nil:n__add:n__sqr:n__dbl:n__first → n__s:n__terms:cons:0:nil:n__add:n__sqr:n__dbl:n__first
activate :: n__s:n__terms:cons:0:nil:n__add:n__sqr:n__dbl:n__first → n__s:n__terms:cons:0:nil:n__add:n__sqr:n__dbl:n__first

Rewrite Strategy: INNERMOST

(7) CompletionProof (UPPER BOUND(ID) transformation)

The transformation into a RNTS is sound, since:

(a) The obligation is a constructor system where every type has a constant constructor,

(b) The following defined symbols do not have to be completely defined, as they can never occur inside other defined symbols:
none

(c) The following functions are completely defined:

activate
dbl
terms
first
s
add
sqr

Due to the following rules being added:
none

And the following fresh constants:

const

(8) Obligation:

Runtime Complexity Weighted TRS where critical functions are completely defined. The underlying TRS is:

Runtime Complexity Weighted TRS with Types.
The TRS R consists of the following rules:

terms(N) → cons(recip(sqr(N)), n__terms(n__s(N))) [1]
sqr(0) → 0 [1]
dbl(0) → 0 [1]
add(0, X) → X [1]
first(0, X) → nil [1]
terms(X) → n__terms(X) [1]
s(X) → n__s(X) [1]
add(X1, X2) → n__add(X1, X2) [1]
sqr(X) → n__sqr(X) [1]
dbl(X) → n__dbl(X) [1]
first(X1, X2) → n__first(X1, X2) [1]
activate(n__terms(X)) → terms(activate(X)) [1]
activate(n__s(X)) → s(X) [1]
activate(n__add(X1, X2)) → add(activate(X1), activate(X2)) [1]
activate(n__sqr(X)) → sqr(activate(X)) [1]
activate(n__dbl(X)) → dbl(activate(X)) [1]
activate(n__first(X1, X2)) → first(activate(X1), activate(X2)) [1]
activate(X) → X [1]

The TRS has the following type information:

Rewrite Strategy: INNERMOST

(9) NarrowingProof (BOTH BOUNDS(ID, ID) transformation)

Narrowed the inner basic terms of all right-hand sides by a single narrowing step.

(10) Obligation:

Runtime Complexity Weighted TRS where critical functions are completely defined. The underlying TRS is:

Runtime Complexity Weighted TRS with Types.
The TRS R consists of the following rules:

terms(N) → cons(recip(sqr(N)), n__terms(n__s(N))) [1]
sqr(0) → 0 [1]
dbl(0) → 0 [1]
add(0, X) → X [1]
first(0, X) → nil [1]
terms(X) → n__terms(X) [1]
s(X) → n__s(X) [1]
add(X1, X2) → n__add(X1, X2) [1]
sqr(X) → n__sqr(X) [1]
dbl(X) → n__dbl(X) [1]
first(X1, X2) → n__first(X1, X2) [1]
activate(n__terms(n__terms(X'))) → terms(terms(activate(X'))) [2]
activate(n__terms(n__s(X''))) → terms(s(X'')) [2]
activate(n__terms(n__add(X1', X2'))) → terms(add(activate(X1'), activate(X2'))) [2]
activate(n__terms(n__sqr(X3))) → terms(sqr(activate(X3))) [2]
activate(n__terms(n__dbl(X4))) → terms(dbl(activate(X4))) [2]
activate(n__terms(n__first(X1'', X2''))) → terms(first(activate(X1''), activate(X2''))) [2]
activate(n__terms(X)) → terms(X) [2]
activate(n__s(X)) → s(X) [1]
activate(n__add(X1, X2)) → add(activate(X1), activate(X2)) [1]
activate(n__sqr(n__terms(X48))) → sqr(terms(activate(X48))) [2]
activate(n__sqr(n__s(X49))) → sqr(s(X49)) [2]
activate(n__sqr(n__add(X121, X220))) → sqr(add(activate(X121), activate(X220))) [2]
activate(n__sqr(n__sqr(X50))) → sqr(sqr(activate(X50))) [2]
activate(n__sqr(n__dbl(X51))) → sqr(dbl(activate(X51))) [2]
activate(n__sqr(n__first(X122, X221))) → sqr(first(activate(X122), activate(X221))) [2]
activate(n__sqr(X)) → sqr(X) [2]
activate(n__dbl(n__terms(X52))) → dbl(terms(activate(X52))) [2]
activate(n__dbl(n__s(X53))) → dbl(s(X53)) [2]
activate(n__dbl(n__add(X123, X222))) → dbl(add(activate(X123), activate(X222))) [2]
activate(n__dbl(n__sqr(X54))) → dbl(sqr(activate(X54))) [2]
activate(n__dbl(n__dbl(X55))) → dbl(dbl(activate(X55))) [2]
activate(n__dbl(n__first(X124, X223))) → dbl(first(activate(X124), activate(X223))) [2]
activate(n__dbl(X)) → dbl(X) [2]
activate(n__first(X1, X2)) → first(activate(X1), activate(X2)) [1]
activate(X) → X [1]

The TRS has the following type information:

Rewrite Strategy: INNERMOST

(11) CpxTypedWeightedTrsToRntsProof (UPPER BOUND(ID) transformation)

Transformed the TRS into an over-approximating RNTS by (improved) Size Abstraction.
The constant constructors are abstracted as follows:

0 => 0
nil => 1
const => 0

(12) Obligation:

Complexity RNTS consisting of the following rules:

activate(z) -{ 1 }→ X :|: X >= 0, z = X
activate(z) -{ 2 }→ terms(X) :|: z = 1 + X, X >= 0
activate(z) -{ 2 }→ terms(terms(activate(X'))) :|: X' >= 0, z = 1 + (1 + X')
activate(z) -{ 2 }→ terms(sqr(activate(X3))) :|: z = 1 + (1 + X3), X3 >= 0
activate(z) -{ 2 }→ terms(s(X'')) :|: z = 1 + (1 + X''), X'' >= 0
activate(z) -{ 2 }→ terms(first(activate(X1''), activate(X2''))) :|: X1'' >= 0, z = 1 + (1 + X1'' + X2''), X2'' >= 0
activate(z) -{ 2 }→ terms(dbl(activate(X4))) :|: z = 1 + (1 + X4), X4 >= 0
activate(z) -{ 2 }→ terms(add(activate(X1'), activate(X2'))) :|: z = 1 + (1 + X1' + X2'), X2' >= 0, X1' >= 0
activate(z) -{ 2 }→ sqr(X) :|: z = 1 + X, X >= 0
activate(z) -{ 2 }→ sqr(terms(activate(X48))) :|: z = 1 + (1 + X48), X48 >= 0
activate(z) -{ 2 }→ sqr(sqr(activate(X50))) :|: X50 >= 0, z = 1 + (1 + X50)
activate(z) -{ 2 }→ sqr(s(X49)) :|: z = 1 + (1 + X49), X49 >= 0
activate(z) -{ 2 }→ sqr(first(activate(X122), activate(X221))) :|: X122 >= 0, X221 >= 0, z = 1 + (1 + X122 + X221)
activate(z) -{ 2 }→ sqr(dbl(activate(X51))) :|: X51 >= 0, z = 1 + (1 + X51)
activate(z) -{ 2 }→ sqr(add(activate(X121), activate(X220))) :|: z = 1 + (1 + X121 + X220), X121 >= 0, X220 >= 0
activate(z) -{ 1 }→ s(X) :|: z = 1 + X, X >= 0
activate(z) -{ 1 }→ first(activate(X1), activate(X2)) :|: X1 >= 0, X2 >= 0, z = 1 + X1 + X2
activate(z) -{ 2 }→ dbl(X) :|: z = 1 + X, X >= 0
activate(z) -{ 2 }→ dbl(terms(activate(X52))) :|: z = 1 + (1 + X52), X52 >= 0
activate(z) -{ 2 }→ dbl(sqr(activate(X54))) :|: z = 1 + (1 + X54), X54 >= 0
activate(z) -{ 2 }→ dbl(s(X53)) :|: z = 1 + (1 + X53), X53 >= 0
activate(z) -{ 2 }→ dbl(first(activate(X124), activate(X223))) :|: X223 >= 0, X124 >= 0, z = 1 + (1 + X124 + X223)
activate(z) -{ 2 }→ dbl(dbl(activate(X55))) :|: z = 1 + (1 + X55), X55 >= 0
activate(z) -{ 2 }→ dbl(add(activate(X123), activate(X222))) :|: z = 1 + (1 + X123 + X222), X222 >= 0, X123 >= 0
activate(z) -{ 1 }→ add(activate(X1), activate(X2)) :|: X1 >= 0, X2 >= 0, z = 1 + X1 + X2
add(z, z') -{ 1 }→ X :|: z' = X, X >= 0, z = 0
add(z, z') -{ 1 }→ 1 + X1 + X2 :|: X1 >= 0, X2 >= 0, z = X1, z' = X2
dbl(z) -{ 1 }→ 0 :|: z = 0
dbl(z) -{ 1 }→ 1 + X :|: X >= 0, z = X
first(z, z') -{ 1 }→ 1 :|: z' = X, X >= 0, z = 0
first(z, z') -{ 1 }→ 1 + X1 + X2 :|: X1 >= 0, X2 >= 0, z = X1, z' = X2
s(z) -{ 1 }→ 1 + X :|: X >= 0, z = X
sqr(z) -{ 1 }→ 0 :|: z = 0
sqr(z) -{ 1 }→ 1 + X :|: X >= 0, z = X
terms(z) -{ 1 }→ 1 + X :|: X >= 0, z = X
terms(z) -{ 1 }→ 1 + (1 + sqr(N)) + (1 + (1 + N)) :|: z = N, N >= 0

(13) InliningProof (UPPER BOUND(ID) transformation)

Inlined the following terminating rules on right-hand sides where appropriate:

sqr(z) -{ 1 }→ 0 :|: z = 0
sqr(z) -{ 1 }→ 1 + X :|: X >= 0, z = X
dbl(z) -{ 1 }→ 0 :|: z = 0
dbl(z) -{ 1 }→ 1 + X :|: X >= 0, z = X
add(z, z') -{ 1 }→ X :|: z' = X, X >= 0, z = 0
add(z, z') -{ 1 }→ 1 + X1 + X2 :|: X1 >= 0, X2 >= 0, z = X1, z' = X2
first(z, z') -{ 1 }→ 1 :|: z' = X, X >= 0, z = 0
first(z, z') -{ 1 }→ 1 + X1 + X2 :|: X1 >= 0, X2 >= 0, z = X1, z' = X2
s(z) -{ 1 }→ 1 + X :|: X >= 0, z = X
terms(z) -{ 1 }→ 1 + (1 + sqr(N)) + (1 + (1 + N)) :|: z = N, N >= 0
terms(z) -{ 1 }→ 1 + X :|: X >= 0, z = X

(14) Obligation:

Complexity RNTS consisting of the following rules:

activate(z) -{ 1 }→ X :|: X >= 0, z = X
activate(z) -{ 2 }→ terms(terms(activate(X'))) :|: X' >= 0, z = 1 + (1 + X')
activate(z) -{ 2 }→ terms(sqr(activate(X3))) :|: z = 1 + (1 + X3), X3 >= 0
activate(z) -{ 2 }→ terms(first(activate(X1''), activate(X2''))) :|: X1'' >= 0, z = 1 + (1 + X1'' + X2''), X2'' >= 0
activate(z) -{ 2 }→ terms(dbl(activate(X4))) :|: z = 1 + (1 + X4), X4 >= 0
activate(z) -{ 2 }→ terms(add(activate(X1'), activate(X2'))) :|: z = 1 + (1 + X1' + X2'), X2' >= 0, X1' >= 0
activate(z) -{ 2 }→ sqr(terms(activate(X48))) :|: z = 1 + (1 + X48), X48 >= 0
activate(z) -{ 2 }→ sqr(sqr(activate(X50))) :|: X50 >= 0, z = 1 + (1 + X50)
activate(z) -{ 2 }→ sqr(first(activate(X122), activate(X221))) :|: X122 >= 0, X221 >= 0, z = 1 + (1 + X122 + X221)
activate(z) -{ 2 }→ sqr(dbl(activate(X51))) :|: X51 >= 0, z = 1 + (1 + X51)
activate(z) -{ 2 }→ sqr(add(activate(X121), activate(X220))) :|: z = 1 + (1 + X121 + X220), X121 >= 0, X220 >= 0
activate(z) -{ 3 }→ sqr(1 + X) :|: z = 1 + (1 + X49), X49 >= 0, X >= 0, X49 = X
activate(z) -{ 1 }→ first(activate(X1), activate(X2)) :|: X1 >= 0, X2 >= 0, z = 1 + X1 + X2
activate(z) -{ 2 }→ dbl(terms(activate(X52))) :|: z = 1 + (1 + X52), X52 >= 0
activate(z) -{ 2 }→ dbl(sqr(activate(X54))) :|: z = 1 + (1 + X54), X54 >= 0
activate(z) -{ 2 }→ dbl(first(activate(X124), activate(X223))) :|: X223 >= 0, X124 >= 0, z = 1 + (1 + X124 + X223)
activate(z) -{ 2 }→ dbl(dbl(activate(X55))) :|: z = 1 + (1 + X55), X55 >= 0
activate(z) -{ 2 }→ dbl(add(activate(X123), activate(X222))) :|: z = 1 + (1 + X123 + X222), X222 >= 0, X123 >= 0
activate(z) -{ 3 }→ dbl(1 + X) :|: z = 1 + (1 + X53), X53 >= 0, X >= 0, X53 = X
activate(z) -{ 1 }→ add(activate(X1), activate(X2)) :|: X1 >= 0, X2 >= 0, z = 1 + X1 + X2
activate(z) -{ 3 }→ 0 :|: z = 1 + X, X >= 0, X = 0
activate(z) -{ 3 }→ 1 + X' :|: z = 1 + X, X >= 0, X' >= 0, X = X'
activate(z) -{ 2 }→ 1 + X' :|: z = 1 + X, X >= 0, X' >= 0, X = X'
activate(z) -{ 4 }→ 1 + X' :|: z = 1 + (1 + X''), X'' >= 0, X >= 0, X'' = X, X' >= 0, 1 + X = X'
activate(z) -{ 3 }→ 1 + (1 + sqr(N)) + (1 + (1 + N)) :|: z = 1 + X, X >= 0, X = N, N >= 0
activate(z) -{ 4 }→ 1 + (1 + sqr(N)) + (1 + (1 + N)) :|: z = 1 + (1 + X''), X'' >= 0, X >= 0, X'' = X, 1 + X = N, N >= 0
add(z, z') -{ 1 }→ X :|: z' = X, X >= 0, z = 0
add(z, z') -{ 1 }→ 1 + X1 + X2 :|: X1 >= 0, X2 >= 0, z = X1, z' = X2
dbl(z) -{ 1 }→ 0 :|: z = 0
dbl(z) -{ 1 }→ 1 + X :|: X >= 0, z = X
first(z, z') -{ 1 }→ 1 :|: z' = X, X >= 0, z = 0
first(z, z') -{ 1 }→ 1 + X1 + X2 :|: X1 >= 0, X2 >= 0, z = X1, z' = X2
s(z) -{ 1 }→ 1 + X :|: X >= 0, z = X
sqr(z) -{ 1 }→ 0 :|: z = 0
sqr(z) -{ 1 }→ 1 + X :|: X >= 0, z = X
terms(z) -{ 1 }→ 1 + X :|: X >= 0, z = X
terms(z) -{ 2 }→ 1 + (1 + 0) + (1 + (1 + N)) :|: z = N, N >= 0, N = 0
terms(z) -{ 2 }→ 1 + (1 + (1 + X)) + (1 + (1 + N)) :|: z = N, N >= 0, X >= 0, N = X

(15) SimplificationProof (BOTH BOUNDS(ID, ID) transformation)

Simplified the RNTS by moving equalities from the constraints into the right-hand sides.

(16) Obligation:

Complexity RNTS consisting of the following rules:

activate(z) -{ 1 }→ z :|: z >= 0
activate(z) -{ 2 }→ terms(terms(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ terms(sqr(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ terms(first(activate(X1''), activate(X2''))) :|: X1'' >= 0, z = 1 + (1 + X1'' + X2''), X2'' >= 0
activate(z) -{ 2 }→ terms(dbl(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ terms(add(activate(X1'), activate(X2'))) :|: z = 1 + (1 + X1' + X2'), X2' >= 0, X1' >= 0
activate(z) -{ 2 }→ sqr(terms(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ sqr(sqr(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ sqr(first(activate(X122), activate(X221))) :|: X122 >= 0, X221 >= 0, z = 1 + (1 + X122 + X221)
activate(z) -{ 2 }→ sqr(dbl(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ sqr(add(activate(X121), activate(X220))) :|: z = 1 + (1 + X121 + X220), X121 >= 0, X220 >= 0
activate(z) -{ 3 }→ sqr(1 + X) :|: z - 2 >= 0, X >= 0, z - 2 = X
activate(z) -{ 1 }→ first(activate(X1), activate(X2)) :|: X1 >= 0, X2 >= 0, z = 1 + X1 + X2
activate(z) -{ 2 }→ dbl(terms(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ dbl(sqr(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ dbl(first(activate(X124), activate(X223))) :|: X223 >= 0, X124 >= 0, z = 1 + (1 + X124 + X223)
activate(z) -{ 2 }→ dbl(dbl(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ dbl(add(activate(X123), activate(X222))) :|: z = 1 + (1 + X123 + X222), X222 >= 0, X123 >= 0
activate(z) -{ 3 }→ dbl(1 + X) :|: z - 2 >= 0, X >= 0, z - 2 = X
activate(z) -{ 1 }→ add(activate(X1), activate(X2)) :|: X1 >= 0, X2 >= 0, z = 1 + X1 + X2
activate(z) -{ 3 }→ 0 :|: z - 1 >= 0, z - 1 = 0
activate(z) -{ 3 }→ 1 + X' :|: z - 1 >= 0, X' >= 0, z - 1 = X'
activate(z) -{ 2 }→ 1 + X' :|: z - 1 >= 0, X' >= 0, z - 1 = X'
activate(z) -{ 4 }→ 1 + X' :|: z - 2 >= 0, X >= 0, z - 2 = X, X' >= 0, 1 + X = X'
activate(z) -{ 3 }→ 1 + (1 + sqr(N)) + (1 + (1 + N)) :|: z - 1 >= 0, z - 1 = N, N >= 0
activate(z) -{ 4 }→ 1 + (1 + sqr(N)) + (1 + (1 + N)) :|: z - 2 >= 0, X >= 0, z - 2 = X, 1 + X = N, N >= 0
add(z, z') -{ 1 }→ z' :|: z' >= 0, z = 0
add(z, z') -{ 1 }→ 1 + z + z' :|: z >= 0, z' >= 0
dbl(z) -{ 1 }→ 0 :|: z = 0
dbl(z) -{ 1 }→ 1 + z :|: z >= 0
first(z, z') -{ 1 }→ 1 :|: z' >= 0, z = 0
first(z, z') -{ 1 }→ 1 + z + z' :|: z >= 0, z' >= 0
s(z) -{ 1 }→ 1 + z :|: z >= 0
sqr(z) -{ 1 }→ 0 :|: z = 0
sqr(z) -{ 1 }→ 1 + z :|: z >= 0
terms(z) -{ 1 }→ 1 + z :|: z >= 0
terms(z) -{ 2 }→ 1 + (1 + 0) + (1 + (1 + z)) :|: z >= 0, z = 0
terms(z) -{ 2 }→ 1 + (1 + (1 + z)) + (1 + (1 + z)) :|: z >= 0

(17) CpxRntsAnalysisOrderProof (BOTH BOUNDS(ID, ID) transformation)

Found the following analysis order by SCC decomposition:

{ first }
{ dbl }
{ terms }
{ add }
{ sqr }
{ s }
{ activate }

(18) Obligation:

Complexity RNTS consisting of the following rules:

activate(z) -{ 1 }→ z :|: z >= 0
activate(z) -{ 2 }→ terms(terms(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ terms(sqr(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ terms(first(activate(X1''), activate(X2''))) :|: X1'' >= 0, z = 1 + (1 + X1'' + X2''), X2'' >= 0
activate(z) -{ 2 }→ terms(dbl(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ terms(add(activate(X1'), activate(X2'))) :|: z = 1 + (1 + X1' + X2'), X2' >= 0, X1' >= 0
activate(z) -{ 2 }→ sqr(terms(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ sqr(sqr(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ sqr(first(activate(X122), activate(X221))) :|: X122 >= 0, X221 >= 0, z = 1 + (1 + X122 + X221)
activate(z) -{ 2 }→ sqr(dbl(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ sqr(add(activate(X121), activate(X220))) :|: z = 1 + (1 + X121 + X220), X121 >= 0, X220 >= 0
activate(z) -{ 3 }→ sqr(1 + X) :|: z - 2 >= 0, X >= 0, z - 2 = X
activate(z) -{ 1 }→ first(activate(X1), activate(X2)) :|: X1 >= 0, X2 >= 0, z = 1 + X1 + X2
activate(z) -{ 2 }→ dbl(terms(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ dbl(sqr(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ dbl(first(activate(X124), activate(X223))) :|: X223 >= 0, X124 >= 0, z = 1 + (1 + X124 + X223)
activate(z) -{ 2 }→ dbl(dbl(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ dbl(add(activate(X123), activate(X222))) :|: z = 1 + (1 + X123 + X222), X222 >= 0, X123 >= 0
activate(z) -{ 3 }→ dbl(1 + X) :|: z - 2 >= 0, X >= 0, z - 2 = X
activate(z) -{ 1 }→ add(activate(X1), activate(X2)) :|: X1 >= 0, X2 >= 0, z = 1 + X1 + X2
activate(z) -{ 3 }→ 0 :|: z - 1 >= 0, z - 1 = 0
activate(z) -{ 3 }→ 1 + X' :|: z - 1 >= 0, X' >= 0, z - 1 = X'
activate(z) -{ 2 }→ 1 + X' :|: z - 1 >= 0, X' >= 0, z - 1 = X'
activate(z) -{ 4 }→ 1 + X' :|: z - 2 >= 0, X >= 0, z - 2 = X, X' >= 0, 1 + X = X'
activate(z) -{ 3 }→ 1 + (1 + sqr(N)) + (1 + (1 + N)) :|: z - 1 >= 0, z - 1 = N, N >= 0
activate(z) -{ 4 }→ 1 + (1 + sqr(N)) + (1 + (1 + N)) :|: z - 2 >= 0, X >= 0, z - 2 = X, 1 + X = N, N >= 0
add(z, z') -{ 1 }→ z' :|: z' >= 0, z = 0
add(z, z') -{ 1 }→ 1 + z + z' :|: z >= 0, z' >= 0
dbl(z) -{ 1 }→ 0 :|: z = 0
dbl(z) -{ 1 }→ 1 + z :|: z >= 0
first(z, z') -{ 1 }→ 1 :|: z' >= 0, z = 0
first(z, z') -{ 1 }→ 1 + z + z' :|: z >= 0, z' >= 0
s(z) -{ 1 }→ 1 + z :|: z >= 0
sqr(z) -{ 1 }→ 0 :|: z = 0
sqr(z) -{ 1 }→ 1 + z :|: z >= 0
terms(z) -{ 1 }→ 1 + z :|: z >= 0
terms(z) -{ 2 }→ 1 + (1 + 0) + (1 + (1 + z)) :|: z >= 0, z = 0
terms(z) -{ 2 }→ 1 + (1 + (1 + z)) + (1 + (1 + z)) :|: z >= 0

Function symbols to be analyzed: {first}, {dbl}, {terms}, {add}, {sqr}, {s}, {activate}

(19) IntTrsBoundProof (UPPER BOUND(ID) transformation)

Computed SIZE bound using CoFloCo for: first
after applying outer abstraction to obtain an ITS,
resulting in: O(n¹) with polynomial bound: 1 + z + z'

(20) Obligation:

Complexity RNTS consisting of the following rules:

activate(z) -{ 1 }→ z :|: z >= 0
activate(z) -{ 2 }→ terms(terms(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ terms(sqr(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ terms(first(activate(X1''), activate(X2''))) :|: X1'' >= 0, z = 1 + (1 + X1'' + X2''), X2'' >= 0
activate(z) -{ 2 }→ terms(dbl(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ terms(add(activate(X1'), activate(X2'))) :|: z = 1 + (1 + X1' + X2'), X2' >= 0, X1' >= 0
activate(z) -{ 2 }→ sqr(terms(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ sqr(sqr(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ sqr(first(activate(X122), activate(X221))) :|: X122 >= 0, X221 >= 0, z = 1 + (1 + X122 + X221)
activate(z) -{ 2 }→ sqr(dbl(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ sqr(add(activate(X121), activate(X220))) :|: z = 1 + (1 + X121 + X220), X121 >= 0, X220 >= 0
activate(z) -{ 3 }→ sqr(1 + X) :|: z - 2 >= 0, X >= 0, z - 2 = X
activate(z) -{ 1 }→ first(activate(X1), activate(X2)) :|: X1 >= 0, X2 >= 0, z = 1 + X1 + X2
activate(z) -{ 2 }→ dbl(terms(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ dbl(sqr(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ dbl(first(activate(X124), activate(X223))) :|: X223 >= 0, X124 >= 0, z = 1 + (1 + X124 + X223)
activate(z) -{ 2 }→ dbl(dbl(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ dbl(add(activate(X123), activate(X222))) :|: z = 1 + (1 + X123 + X222), X222 >= 0, X123 >= 0
activate(z) -{ 3 }→ dbl(1 + X) :|: z - 2 >= 0, X >= 0, z - 2 = X
activate(z) -{ 1 }→ add(activate(X1), activate(X2)) :|: X1 >= 0, X2 >= 0, z = 1 + X1 + X2
activate(z) -{ 3 }→ 0 :|: z - 1 >= 0, z - 1 = 0
activate(z) -{ 3 }→ 1 + X' :|: z - 1 >= 0, X' >= 0, z - 1 = X'
activate(z) -{ 2 }→ 1 + X' :|: z - 1 >= 0, X' >= 0, z - 1 = X'
activate(z) -{ 4 }→ 1 + X' :|: z - 2 >= 0, X >= 0, z - 2 = X, X' >= 0, 1 + X = X'
activate(z) -{ 3 }→ 1 + (1 + sqr(N)) + (1 + (1 + N)) :|: z - 1 >= 0, z - 1 = N, N >= 0
activate(z) -{ 4 }→ 1 + (1 + sqr(N)) + (1 + (1 + N)) :|: z - 2 >= 0, X >= 0, z - 2 = X, 1 + X = N, N >= 0
add(z, z') -{ 1 }→ z' :|: z' >= 0, z = 0
add(z, z') -{ 1 }→ 1 + z + z' :|: z >= 0, z' >= 0
dbl(z) -{ 1 }→ 0 :|: z = 0
dbl(z) -{ 1 }→ 1 + z :|: z >= 0
first(z, z') -{ 1 }→ 1 :|: z' >= 0, z = 0
first(z, z') -{ 1 }→ 1 + z + z' :|: z >= 0, z' >= 0
s(z) -{ 1 }→ 1 + z :|: z >= 0
sqr(z) -{ 1 }→ 0 :|: z = 0
sqr(z) -{ 1 }→ 1 + z :|: z >= 0
terms(z) -{ 1 }→ 1 + z :|: z >= 0
terms(z) -{ 2 }→ 1 + (1 + 0) + (1 + (1 + z)) :|: z >= 0, z = 0
terms(z) -{ 2 }→ 1 + (1 + (1 + z)) + (1 + (1 + z)) :|: z >= 0

Function symbols to be analyzed: {first}, {dbl}, {terms}, {add}, {sqr}, {s}, {activate}
Previous analysis results are:

first: runtime: ?, size: O(n¹) [1 + z + z']

(21) IntTrsBoundProof (UPPER BOUND(ID) transformation)

Computed RUNTIME bound using CoFloCo for: first
after applying outer abstraction to obtain an ITS,
resulting in: O(1) with polynomial bound: 1

(22) Obligation:

Complexity RNTS consisting of the following rules:

activate(z) -{ 1 }→ z :|: z >= 0
activate(z) -{ 2 }→ terms(terms(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ terms(sqr(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ terms(first(activate(X1''), activate(X2''))) :|: X1'' >= 0, z = 1 + (1 + X1'' + X2''), X2'' >= 0
activate(z) -{ 2 }→ terms(dbl(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ terms(add(activate(X1'), activate(X2'))) :|: z = 1 + (1 + X1' + X2'), X2' >= 0, X1' >= 0
activate(z) -{ 2 }→ sqr(terms(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ sqr(sqr(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ sqr(first(activate(X122), activate(X221))) :|: X122 >= 0, X221 >= 0, z = 1 + (1 + X122 + X221)
activate(z) -{ 2 }→ sqr(dbl(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ sqr(add(activate(X121), activate(X220))) :|: z = 1 + (1 + X121 + X220), X121 >= 0, X220 >= 0
activate(z) -{ 3 }→ sqr(1 + X) :|: z - 2 >= 0, X >= 0, z - 2 = X
activate(z) -{ 1 }→ first(activate(X1), activate(X2)) :|: X1 >= 0, X2 >= 0, z = 1 + X1 + X2
activate(z) -{ 2 }→ dbl(terms(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ dbl(sqr(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ dbl(first(activate(X124), activate(X223))) :|: X223 >= 0, X124 >= 0, z = 1 + (1 + X124 + X223)
activate(z) -{ 2 }→ dbl(dbl(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ dbl(add(activate(X123), activate(X222))) :|: z = 1 + (1 + X123 + X222), X222 >= 0, X123 >= 0
activate(z) -{ 3 }→ dbl(1 + X) :|: z - 2 >= 0, X >= 0, z - 2 = X
activate(z) -{ 1 }→ add(activate(X1), activate(X2)) :|: X1 >= 0, X2 >= 0, z = 1 + X1 + X2
activate(z) -{ 3 }→ 0 :|: z - 1 >= 0, z - 1 = 0
activate(z) -{ 3 }→ 1 + X' :|: z - 1 >= 0, X' >= 0, z - 1 = X'
activate(z) -{ 2 }→ 1 + X' :|: z - 1 >= 0, X' >= 0, z - 1 = X'
activate(z) -{ 4 }→ 1 + X' :|: z - 2 >= 0, X >= 0, z - 2 = X, X' >= 0, 1 + X = X'
activate(z) -{ 3 }→ 1 + (1 + sqr(N)) + (1 + (1 + N)) :|: z - 1 >= 0, z - 1 = N, N >= 0
activate(z) -{ 4 }→ 1 + (1 + sqr(N)) + (1 + (1 + N)) :|: z - 2 >= 0, X >= 0, z - 2 = X, 1 + X = N, N >= 0
add(z, z') -{ 1 }→ z' :|: z' >= 0, z = 0
add(z, z') -{ 1 }→ 1 + z + z' :|: z >= 0, z' >= 0
dbl(z) -{ 1 }→ 0 :|: z = 0
dbl(z) -{ 1 }→ 1 + z :|: z >= 0
first(z, z') -{ 1 }→ 1 :|: z' >= 0, z = 0
first(z, z') -{ 1 }→ 1 + z + z' :|: z >= 0, z' >= 0
s(z) -{ 1 }→ 1 + z :|: z >= 0
sqr(z) -{ 1 }→ 0 :|: z = 0
sqr(z) -{ 1 }→ 1 + z :|: z >= 0
terms(z) -{ 1 }→ 1 + z :|: z >= 0
terms(z) -{ 2 }→ 1 + (1 + 0) + (1 + (1 + z)) :|: z >= 0, z = 0
terms(z) -{ 2 }→ 1 + (1 + (1 + z)) + (1 + (1 + z)) :|: z >= 0

Function symbols to be analyzed: {dbl}, {terms}, {add}, {sqr}, {s}, {activate}
Previous analysis results are:

first: runtime: O(1) [1], size: O(n¹) [1 + z + z']

(23) ResultPropagationProof (UPPER BOUND(ID) transformation)

Applied inner abstraction using the recently inferred runtime/size bounds where possible.

(24) Obligation:

Complexity RNTS consisting of the following rules:

activate(z) -{ 1 }→ z :|: z >= 0
activate(z) -{ 2 }→ terms(terms(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ terms(sqr(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ terms(first(activate(X1''), activate(X2''))) :|: X1'' >= 0, z = 1 + (1 + X1'' + X2''), X2'' >= 0
activate(z) -{ 2 }→ terms(dbl(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ terms(add(activate(X1'), activate(X2'))) :|: z = 1 + (1 + X1' + X2'), X2' >= 0, X1' >= 0
activate(z) -{ 2 }→ sqr(terms(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ sqr(sqr(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ sqr(first(activate(X122), activate(X221))) :|: X122 >= 0, X221 >= 0, z = 1 + (1 + X122 + X221)
activate(z) -{ 2 }→ sqr(dbl(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ sqr(add(activate(X121), activate(X220))) :|: z = 1 + (1 + X121 + X220), X121 >= 0, X220 >= 0
activate(z) -{ 3 }→ sqr(1 + X) :|: z - 2 >= 0, X >= 0, z - 2 = X
activate(z) -{ 1 }→ first(activate(X1), activate(X2)) :|: X1 >= 0, X2 >= 0, z = 1 + X1 + X2
activate(z) -{ 2 }→ dbl(terms(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ dbl(sqr(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ dbl(first(activate(X124), activate(X223))) :|: X223 >= 0, X124 >= 0, z = 1 + (1 + X124 + X223)
activate(z) -{ 2 }→ dbl(dbl(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ dbl(add(activate(X123), activate(X222))) :|: z = 1 + (1 + X123 + X222), X222 >= 0, X123 >= 0
activate(z) -{ 3 }→ dbl(1 + X) :|: z - 2 >= 0, X >= 0, z - 2 = X
activate(z) -{ 1 }→ add(activate(X1), activate(X2)) :|: X1 >= 0, X2 >= 0, z = 1 + X1 + X2
activate(z) -{ 3 }→ 0 :|: z - 1 >= 0, z - 1 = 0
activate(z) -{ 3 }→ 1 + X' :|: z - 1 >= 0, X' >= 0, z - 1 = X'
activate(z) -{ 2 }→ 1 + X' :|: z - 1 >= 0, X' >= 0, z - 1 = X'
activate(z) -{ 4 }→ 1 + X' :|: z - 2 >= 0, X >= 0, z - 2 = X, X' >= 0, 1 + X = X'
activate(z) -{ 3 }→ 1 + (1 + sqr(N)) + (1 + (1 + N)) :|: z - 1 >= 0, z - 1 = N, N >= 0
activate(z) -{ 4 }→ 1 + (1 + sqr(N)) + (1 + (1 + N)) :|: z - 2 >= 0, X >= 0, z - 2 = X, 1 + X = N, N >= 0
add(z, z') -{ 1 }→ z' :|: z' >= 0, z = 0
add(z, z') -{ 1 }→ 1 + z + z' :|: z >= 0, z' >= 0
dbl(z) -{ 1 }→ 0 :|: z = 0
dbl(z) -{ 1 }→ 1 + z :|: z >= 0
first(z, z') -{ 1 }→ 1 :|: z' >= 0, z = 0
first(z, z') -{ 1 }→ 1 + z + z' :|: z >= 0, z' >= 0
s(z) -{ 1 }→ 1 + z :|: z >= 0
sqr(z) -{ 1 }→ 0 :|: z = 0
sqr(z) -{ 1 }→ 1 + z :|: z >= 0
terms(z) -{ 1 }→ 1 + z :|: z >= 0
terms(z) -{ 2 }→ 1 + (1 + 0) + (1 + (1 + z)) :|: z >= 0, z = 0
terms(z) -{ 2 }→ 1 + (1 + (1 + z)) + (1 + (1 + z)) :|: z >= 0

Function symbols to be analyzed: {dbl}, {terms}, {add}, {sqr}, {s}, {activate}
Previous analysis results are:

first: runtime: O(1) [1], size: O(n¹) [1 + z + z']

(25) IntTrsBoundProof (UPPER BOUND(ID) transformation)

Computed SIZE bound using CoFloCo for: dbl
after applying outer abstraction to obtain an ITS,
resulting in: O(n¹) with polynomial bound: 1 + z

(26) Obligation:

Complexity RNTS consisting of the following rules:

activate(z) -{ 1 }→ z :|: z >= 0
activate(z) -{ 2 }→ terms(terms(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ terms(sqr(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ terms(first(activate(X1''), activate(X2''))) :|: X1'' >= 0, z = 1 + (1 + X1'' + X2''), X2'' >= 0
activate(z) -{ 2 }→ terms(dbl(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ terms(add(activate(X1'), activate(X2'))) :|: z = 1 + (1 + X1' + X2'), X2' >= 0, X1' >= 0
activate(z) -{ 2 }→ sqr(terms(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ sqr(sqr(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ sqr(first(activate(X122), activate(X221))) :|: X122 >= 0, X221 >= 0, z = 1 + (1 + X122 + X221)
activate(z) -{ 2 }→ sqr(dbl(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ sqr(add(activate(X121), activate(X220))) :|: z = 1 + (1 + X121 + X220), X121 >= 0, X220 >= 0
activate(z) -{ 3 }→ sqr(1 + X) :|: z - 2 >= 0, X >= 0, z - 2 = X
activate(z) -{ 1 }→ first(activate(X1), activate(X2)) :|: X1 >= 0, X2 >= 0, z = 1 + X1 + X2
activate(z) -{ 2 }→ dbl(terms(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ dbl(sqr(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ dbl(first(activate(X124), activate(X223))) :|: X223 >= 0, X124 >= 0, z = 1 + (1 + X124 + X223)
activate(z) -{ 2 }→ dbl(dbl(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ dbl(add(activate(X123), activate(X222))) :|: z = 1 + (1 + X123 + X222), X222 >= 0, X123 >= 0
activate(z) -{ 3 }→ dbl(1 + X) :|: z - 2 >= 0, X >= 0, z - 2 = X
activate(z) -{ 1 }→ add(activate(X1), activate(X2)) :|: X1 >= 0, X2 >= 0, z = 1 + X1 + X2
activate(z) -{ 3 }→ 0 :|: z - 1 >= 0, z - 1 = 0
activate(z) -{ 3 }→ 1 + X' :|: z - 1 >= 0, X' >= 0, z - 1 = X'
activate(z) -{ 2 }→ 1 + X' :|: z - 1 >= 0, X' >= 0, z - 1 = X'
activate(z) -{ 4 }→ 1 + X' :|: z - 2 >= 0, X >= 0, z - 2 = X, X' >= 0, 1 + X = X'
activate(z) -{ 3 }→ 1 + (1 + sqr(N)) + (1 + (1 + N)) :|: z - 1 >= 0, z - 1 = N, N >= 0
activate(z) -{ 4 }→ 1 + (1 + sqr(N)) + (1 + (1 + N)) :|: z - 2 >= 0, X >= 0, z - 2 = X, 1 + X = N, N >= 0
add(z, z') -{ 1 }→ z' :|: z' >= 0, z = 0
add(z, z') -{ 1 }→ 1 + z + z' :|: z >= 0, z' >= 0
dbl(z) -{ 1 }→ 0 :|: z = 0
dbl(z) -{ 1 }→ 1 + z :|: z >= 0
first(z, z') -{ 1 }→ 1 :|: z' >= 0, z = 0
first(z, z') -{ 1 }→ 1 + z + z' :|: z >= 0, z' >= 0
s(z) -{ 1 }→ 1 + z :|: z >= 0
sqr(z) -{ 1 }→ 0 :|: z = 0
sqr(z) -{ 1 }→ 1 + z :|: z >= 0
terms(z) -{ 1 }→ 1 + z :|: z >= 0
terms(z) -{ 2 }→ 1 + (1 + 0) + (1 + (1 + z)) :|: z >= 0, z = 0
terms(z) -{ 2 }→ 1 + (1 + (1 + z)) + (1 + (1 + z)) :|: z >= 0

Function symbols to be analyzed: {dbl}, {terms}, {add}, {sqr}, {s}, {activate}
Previous analysis results are:

first: runtime: O(1) [1], size: O(n¹) [1 + z + z']
dbl: runtime: ?, size: O(n¹) [1 + z]

(27) IntTrsBoundProof (UPPER BOUND(ID) transformation)

Computed RUNTIME bound using CoFloCo for: dbl
after applying outer abstraction to obtain an ITS,
resulting in: O(1) with polynomial bound: 1

(28) Obligation:

Complexity RNTS consisting of the following rules:

activate(z) -{ 1 }→ z :|: z >= 0
activate(z) -{ 2 }→ terms(terms(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ terms(sqr(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ terms(first(activate(X1''), activate(X2''))) :|: X1'' >= 0, z = 1 + (1 + X1'' + X2''), X2'' >= 0
activate(z) -{ 2 }→ terms(dbl(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ terms(add(activate(X1'), activate(X2'))) :|: z = 1 + (1 + X1' + X2'), X2' >= 0, X1' >= 0
activate(z) -{ 2 }→ sqr(terms(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ sqr(sqr(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ sqr(first(activate(X122), activate(X221))) :|: X122 >= 0, X221 >= 0, z = 1 + (1 + X122 + X221)
activate(z) -{ 2 }→ sqr(dbl(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ sqr(add(activate(X121), activate(X220))) :|: z = 1 + (1 + X121 + X220), X121 >= 0, X220 >= 0
activate(z) -{ 3 }→ sqr(1 + X) :|: z - 2 >= 0, X >= 0, z - 2 = X
activate(z) -{ 1 }→ first(activate(X1), activate(X2)) :|: X1 >= 0, X2 >= 0, z = 1 + X1 + X2
activate(z) -{ 2 }→ dbl(terms(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ dbl(sqr(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ dbl(first(activate(X124), activate(X223))) :|: X223 >= 0, X124 >= 0, z = 1 + (1 + X124 + X223)
activate(z) -{ 2 }→ dbl(dbl(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ dbl(add(activate(X123), activate(X222))) :|: z = 1 + (1 + X123 + X222), X222 >= 0, X123 >= 0
activate(z) -{ 3 }→ dbl(1 + X) :|: z - 2 >= 0, X >= 0, z - 2 = X
activate(z) -{ 1 }→ add(activate(X1), activate(X2)) :|: X1 >= 0, X2 >= 0, z = 1 + X1 + X2
activate(z) -{ 3 }→ 0 :|: z - 1 >= 0, z - 1 = 0
activate(z) -{ 3 }→ 1 + X' :|: z - 1 >= 0, X' >= 0, z - 1 = X'
activate(z) -{ 2 }→ 1 + X' :|: z - 1 >= 0, X' >= 0, z - 1 = X'
activate(z) -{ 4 }→ 1 + X' :|: z - 2 >= 0, X >= 0, z - 2 = X, X' >= 0, 1 + X = X'
activate(z) -{ 3 }→ 1 + (1 + sqr(N)) + (1 + (1 + N)) :|: z - 1 >= 0, z - 1 = N, N >= 0
activate(z) -{ 4 }→ 1 + (1 + sqr(N)) + (1 + (1 + N)) :|: z - 2 >= 0, X >= 0, z - 2 = X, 1 + X = N, N >= 0
add(z, z') -{ 1 }→ z' :|: z' >= 0, z = 0
add(z, z') -{ 1 }→ 1 + z + z' :|: z >= 0, z' >= 0
dbl(z) -{ 1 }→ 0 :|: z = 0
dbl(z) -{ 1 }→ 1 + z :|: z >= 0
first(z, z') -{ 1 }→ 1 :|: z' >= 0, z = 0
first(z, z') -{ 1 }→ 1 + z + z' :|: z >= 0, z' >= 0
s(z) -{ 1 }→ 1 + z :|: z >= 0
sqr(z) -{ 1 }→ 0 :|: z = 0
sqr(z) -{ 1 }→ 1 + z :|: z >= 0
terms(z) -{ 1 }→ 1 + z :|: z >= 0
terms(z) -{ 2 }→ 1 + (1 + 0) + (1 + (1 + z)) :|: z >= 0, z = 0
terms(z) -{ 2 }→ 1 + (1 + (1 + z)) + (1 + (1 + z)) :|: z >= 0

Function symbols to be analyzed: {terms}, {add}, {sqr}, {s}, {activate}
Previous analysis results are:

first: runtime: O(1) [1], size: O(n¹) [1 + z + z']
dbl: runtime: O(1) [1], size: O(n¹) [1 + z]

(29) ResultPropagationProof (UPPER BOUND(ID) transformation)

Applied inner abstraction using the recently inferred runtime/size bounds where possible.

(30) Obligation:

Complexity RNTS consisting of the following rules:

activate(z) -{ 4 }→ s :|: s >= 0, s <= 1 * (1 + X) + 1, z - 2 >= 0, X >= 0, z - 2 = X
activate(z) -{ 1 }→ z :|: z >= 0
activate(z) -{ 2 }→ terms(terms(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ terms(sqr(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ terms(first(activate(X1''), activate(X2''))) :|: X1'' >= 0, z = 1 + (1 + X1'' + X2''), X2'' >= 0
activate(z) -{ 2 }→ terms(dbl(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ terms(add(activate(X1'), activate(X2'))) :|: z = 1 + (1 + X1' + X2'), X2' >= 0, X1' >= 0
activate(z) -{ 2 }→ sqr(terms(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ sqr(sqr(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ sqr(first(activate(X122), activate(X221))) :|: X122 >= 0, X221 >= 0, z = 1 + (1 + X122 + X221)
activate(z) -{ 2 }→ sqr(dbl(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ sqr(add(activate(X121), activate(X220))) :|: z = 1 + (1 + X121 + X220), X121 >= 0, X220 >= 0
activate(z) -{ 3 }→ sqr(1 + X) :|: z - 2 >= 0, X >= 0, z - 2 = X
activate(z) -{ 1 }→ first(activate(X1), activate(X2)) :|: X1 >= 0, X2 >= 0, z = 1 + X1 + X2
activate(z) -{ 2 }→ dbl(terms(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ dbl(sqr(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ dbl(first(activate(X124), activate(X223))) :|: X223 >= 0, X124 >= 0, z = 1 + (1 + X124 + X223)
activate(z) -{ 2 }→ dbl(dbl(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ dbl(add(activate(X123), activate(X222))) :|: z = 1 + (1 + X123 + X222), X222 >= 0, X123 >= 0
activate(z) -{ 1 }→ add(activate(X1), activate(X2)) :|: X1 >= 0, X2 >= 0, z = 1 + X1 + X2
activate(z) -{ 3 }→ 0 :|: z - 1 >= 0, z - 1 = 0
activate(z) -{ 3 }→ 1 + X' :|: z - 1 >= 0, X' >= 0, z - 1 = X'
activate(z) -{ 2 }→ 1 + X' :|: z - 1 >= 0, X' >= 0, z - 1 = X'
activate(z) -{ 4 }→ 1 + X' :|: z - 2 >= 0, X >= 0, z - 2 = X, X' >= 0, 1 + X = X'
activate(z) -{ 3 }→ 1 + (1 + sqr(N)) + (1 + (1 + N)) :|: z - 1 >= 0, z - 1 = N, N >= 0
activate(z) -{ 4 }→ 1 + (1 + sqr(N)) + (1 + (1 + N)) :|: z - 2 >= 0, X >= 0, z - 2 = X, 1 + X = N, N >= 0
add(z, z') -{ 1 }→ z' :|: z' >= 0, z = 0
add(z, z') -{ 1 }→ 1 + z + z' :|: z >= 0, z' >= 0
dbl(z) -{ 1 }→ 0 :|: z = 0
dbl(z) -{ 1 }→ 1 + z :|: z >= 0
first(z, z') -{ 1 }→ 1 :|: z' >= 0, z = 0
first(z, z') -{ 1 }→ 1 + z + z' :|: z >= 0, z' >= 0
s(z) -{ 1 }→ 1 + z :|: z >= 0
sqr(z) -{ 1 }→ 0 :|: z = 0
sqr(z) -{ 1 }→ 1 + z :|: z >= 0
terms(z) -{ 1 }→ 1 + z :|: z >= 0
terms(z) -{ 2 }→ 1 + (1 + 0) + (1 + (1 + z)) :|: z >= 0, z = 0
terms(z) -{ 2 }→ 1 + (1 + (1 + z)) + (1 + (1 + z)) :|: z >= 0

Function symbols to be analyzed: {terms}, {add}, {sqr}, {s}, {activate}
Previous analysis results are:

first: runtime: O(1) [1], size: O(n¹) [1 + z + z']
dbl: runtime: O(1) [1], size: O(n¹) [1 + z]

(31) IntTrsBoundProof (UPPER BOUND(ID) transformation)

Computed SIZE bound using CoFloCo for: terms
after applying outer abstraction to obtain an ITS,
resulting in: O(n¹) with polynomial bound: 5 + 2·z

(32) Obligation:

Complexity RNTS consisting of the following rules:

activate(z) -{ 4 }→ s :|: s >= 0, s <= 1 * (1 + X) + 1, z - 2 >= 0, X >= 0, z - 2 = X
activate(z) -{ 1 }→ z :|: z >= 0
activate(z) -{ 2 }→ terms(terms(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ terms(sqr(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ terms(first(activate(X1''), activate(X2''))) :|: X1'' >= 0, z = 1 + (1 + X1'' + X2''), X2'' >= 0
activate(z) -{ 2 }→ terms(dbl(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ terms(add(activate(X1'), activate(X2'))) :|: z = 1 + (1 + X1' + X2'), X2' >= 0, X1' >= 0
activate(z) -{ 2 }→ sqr(terms(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ sqr(sqr(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ sqr(first(activate(X122), activate(X221))) :|: X122 >= 0, X221 >= 0, z = 1 + (1 + X122 + X221)
activate(z) -{ 2 }→ sqr(dbl(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ sqr(add(activate(X121), activate(X220))) :|: z = 1 + (1 + X121 + X220), X121 >= 0, X220 >= 0
activate(z) -{ 3 }→ sqr(1 + X) :|: z - 2 >= 0, X >= 0, z - 2 = X
activate(z) -{ 1 }→ first(activate(X1), activate(X2)) :|: X1 >= 0, X2 >= 0, z = 1 + X1 + X2
activate(z) -{ 2 }→ dbl(terms(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ dbl(sqr(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ dbl(first(activate(X124), activate(X223))) :|: X223 >= 0, X124 >= 0, z = 1 + (1 + X124 + X223)
activate(z) -{ 2 }→ dbl(dbl(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ dbl(add(activate(X123), activate(X222))) :|: z = 1 + (1 + X123 + X222), X222 >= 0, X123 >= 0
activate(z) -{ 1 }→ add(activate(X1), activate(X2)) :|: X1 >= 0, X2 >= 0, z = 1 + X1 + X2
activate(z) -{ 3 }→ 0 :|: z - 1 >= 0, z - 1 = 0
activate(z) -{ 3 }→ 1 + X' :|: z - 1 >= 0, X' >= 0, z - 1 = X'
activate(z) -{ 2 }→ 1 + X' :|: z - 1 >= 0, X' >= 0, z - 1 = X'
activate(z) -{ 4 }→ 1 + X' :|: z - 2 >= 0, X >= 0, z - 2 = X, X' >= 0, 1 + X = X'
activate(z) -{ 3 }→ 1 + (1 + sqr(N)) + (1 + (1 + N)) :|: z - 1 >= 0, z - 1 = N, N >= 0
activate(z) -{ 4 }→ 1 + (1 + sqr(N)) + (1 + (1 + N)) :|: z - 2 >= 0, X >= 0, z - 2 = X, 1 + X = N, N >= 0
add(z, z') -{ 1 }→ z' :|: z' >= 0, z = 0
add(z, z') -{ 1 }→ 1 + z + z' :|: z >= 0, z' >= 0
dbl(z) -{ 1 }→ 0 :|: z = 0
dbl(z) -{ 1 }→ 1 + z :|: z >= 0
first(z, z') -{ 1 }→ 1 :|: z' >= 0, z = 0
first(z, z') -{ 1 }→ 1 + z + z' :|: z >= 0, z' >= 0
s(z) -{ 1 }→ 1 + z :|: z >= 0
sqr(z) -{ 1 }→ 0 :|: z = 0
sqr(z) -{ 1 }→ 1 + z :|: z >= 0
terms(z) -{ 1 }→ 1 + z :|: z >= 0
terms(z) -{ 2 }→ 1 + (1 + 0) + (1 + (1 + z)) :|: z >= 0, z = 0
terms(z) -{ 2 }→ 1 + (1 + (1 + z)) + (1 + (1 + z)) :|: z >= 0

Function symbols to be analyzed: {terms}, {add}, {sqr}, {s}, {activate}
Previous analysis results are:

first: runtime: O(1) [1], size: O(n¹) [1 + z + z']
dbl: runtime: O(1) [1], size: O(n¹) [1 + z]
terms: runtime: ?, size: O(n¹) [5 + 2·z]

(33) IntTrsBoundProof (UPPER BOUND(ID) transformation)

Computed RUNTIME bound using CoFloCo for: terms
after applying outer abstraction to obtain an ITS,
resulting in: O(1) with polynomial bound: 2

(34) Obligation:

Complexity RNTS consisting of the following rules:

activate(z) -{ 4 }→ s :|: s >= 0, s <= 1 * (1 + X) + 1, z - 2 >= 0, X >= 0, z - 2 = X
activate(z) -{ 1 }→ z :|: z >= 0
activate(z) -{ 2 }→ terms(terms(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ terms(sqr(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ terms(first(activate(X1''), activate(X2''))) :|: X1'' >= 0, z = 1 + (1 + X1'' + X2''), X2'' >= 0
activate(z) -{ 2 }→ terms(dbl(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ terms(add(activate(X1'), activate(X2'))) :|: z = 1 + (1 + X1' + X2'), X2' >= 0, X1' >= 0
activate(z) -{ 2 }→ sqr(terms(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ sqr(sqr(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ sqr(first(activate(X122), activate(X221))) :|: X122 >= 0, X221 >= 0, z = 1 + (1 + X122 + X221)
activate(z) -{ 2 }→ sqr(dbl(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ sqr(add(activate(X121), activate(X220))) :|: z = 1 + (1 + X121 + X220), X121 >= 0, X220 >= 0
activate(z) -{ 3 }→ sqr(1 + X) :|: z - 2 >= 0, X >= 0, z - 2 = X
activate(z) -{ 1 }→ first(activate(X1), activate(X2)) :|: X1 >= 0, X2 >= 0, z = 1 + X1 + X2
activate(z) -{ 2 }→ dbl(terms(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ dbl(sqr(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ dbl(first(activate(X124), activate(X223))) :|: X223 >= 0, X124 >= 0, z = 1 + (1 + X124 + X223)
activate(z) -{ 2 }→ dbl(dbl(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ dbl(add(activate(X123), activate(X222))) :|: z = 1 + (1 + X123 + X222), X222 >= 0, X123 >= 0
activate(z) -{ 1 }→ add(activate(X1), activate(X2)) :|: X1 >= 0, X2 >= 0, z = 1 + X1 + X2
activate(z) -{ 3 }→ 0 :|: z - 1 >= 0, z - 1 = 0
activate(z) -{ 3 }→ 1 + X' :|: z - 1 >= 0, X' >= 0, z - 1 = X'
activate(z) -{ 2 }→ 1 + X' :|: z - 1 >= 0, X' >= 0, z - 1 = X'
activate(z) -{ 4 }→ 1 + X' :|: z - 2 >= 0, X >= 0, z - 2 = X, X' >= 0, 1 + X = X'
activate(z) -{ 3 }→ 1 + (1 + sqr(N)) + (1 + (1 + N)) :|: z - 1 >= 0, z - 1 = N, N >= 0
activate(z) -{ 4 }→ 1 + (1 + sqr(N)) + (1 + (1 + N)) :|: z - 2 >= 0, X >= 0, z - 2 = X, 1 + X = N, N >= 0
add(z, z') -{ 1 }→ z' :|: z' >= 0, z = 0
add(z, z') -{ 1 }→ 1 + z + z' :|: z >= 0, z' >= 0
dbl(z) -{ 1 }→ 0 :|: z = 0
dbl(z) -{ 1 }→ 1 + z :|: z >= 0
first(z, z') -{ 1 }→ 1 :|: z' >= 0, z = 0
first(z, z') -{ 1 }→ 1 + z + z' :|: z >= 0, z' >= 0
s(z) -{ 1 }→ 1 + z :|: z >= 0
sqr(z) -{ 1 }→ 0 :|: z = 0
sqr(z) -{ 1 }→ 1 + z :|: z >= 0
terms(z) -{ 1 }→ 1 + z :|: z >= 0
terms(z) -{ 2 }→ 1 + (1 + 0) + (1 + (1 + z)) :|: z >= 0, z = 0
terms(z) -{ 2 }→ 1 + (1 + (1 + z)) + (1 + (1 + z)) :|: z >= 0

Function symbols to be analyzed: {add}, {sqr}, {s}, {activate}
Previous analysis results are:

first: runtime: O(1) [1], size: O(n¹) [1 + z + z']
dbl: runtime: O(1) [1], size: O(n¹) [1 + z]
terms: runtime: O(1) [2], size: O(n¹) [5 + 2·z]

(35) ResultPropagationProof (UPPER BOUND(ID) transformation)

Applied inner abstraction using the recently inferred runtime/size bounds where possible.

(36) Obligation:

Complexity RNTS consisting of the following rules:

activate(z) -{ 4 }→ s :|: s >= 0, s <= 1 * (1 + X) + 1, z - 2 >= 0, X >= 0, z - 2 = X
activate(z) -{ 1 }→ z :|: z >= 0
activate(z) -{ 2 }→ terms(terms(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ terms(sqr(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ terms(first(activate(X1''), activate(X2''))) :|: X1'' >= 0, z = 1 + (1 + X1'' + X2''), X2'' >= 0
activate(z) -{ 2 }→ terms(dbl(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ terms(add(activate(X1'), activate(X2'))) :|: z = 1 + (1 + X1' + X2'), X2' >= 0, X1' >= 0
activate(z) -{ 2 }→ sqr(terms(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ sqr(sqr(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ sqr(first(activate(X122), activate(X221))) :|: X122 >= 0, X221 >= 0, z = 1 + (1 + X122 + X221)
activate(z) -{ 2 }→ sqr(dbl(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ sqr(add(activate(X121), activate(X220))) :|: z = 1 + (1 + X121 + X220), X121 >= 0, X220 >= 0
activate(z) -{ 3 }→ sqr(1 + X) :|: z - 2 >= 0, X >= 0, z - 2 = X
activate(z) -{ 1 }→ first(activate(X1), activate(X2)) :|: X1 >= 0, X2 >= 0, z = 1 + X1 + X2
activate(z) -{ 2 }→ dbl(terms(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ dbl(sqr(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ dbl(first(activate(X124), activate(X223))) :|: X223 >= 0, X124 >= 0, z = 1 + (1 + X124 + X223)
activate(z) -{ 2 }→ dbl(dbl(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ dbl(add(activate(X123), activate(X222))) :|: z = 1 + (1 + X123 + X222), X222 >= 0, X123 >= 0
activate(z) -{ 1 }→ add(activate(X1), activate(X2)) :|: X1 >= 0, X2 >= 0, z = 1 + X1 + X2
activate(z) -{ 3 }→ 0 :|: z - 1 >= 0, z - 1 = 0
activate(z) -{ 3 }→ 1 + X' :|: z - 1 >= 0, X' >= 0, z - 1 = X'
activate(z) -{ 2 }→ 1 + X' :|: z - 1 >= 0, X' >= 0, z - 1 = X'
activate(z) -{ 4 }→ 1 + X' :|: z - 2 >= 0, X >= 0, z - 2 = X, X' >= 0, 1 + X = X'
activate(z) -{ 3 }→ 1 + (1 + sqr(N)) + (1 + (1 + N)) :|: z - 1 >= 0, z - 1 = N, N >= 0
activate(z) -{ 4 }→ 1 + (1 + sqr(N)) + (1 + (1 + N)) :|: z - 2 >= 0, X >= 0, z - 2 = X, 1 + X = N, N >= 0
add(z, z') -{ 1 }→ z' :|: z' >= 0, z = 0
add(z, z') -{ 1 }→ 1 + z + z' :|: z >= 0, z' >= 0
dbl(z) -{ 1 }→ 0 :|: z = 0
dbl(z) -{ 1 }→ 1 + z :|: z >= 0
first(z, z') -{ 1 }→ 1 :|: z' >= 0, z = 0
first(z, z') -{ 1 }→ 1 + z + z' :|: z >= 0, z' >= 0
s(z) -{ 1 }→ 1 + z :|: z >= 0
sqr(z) -{ 1 }→ 0 :|: z = 0
sqr(z) -{ 1 }→ 1 + z :|: z >= 0
terms(z) -{ 1 }→ 1 + z :|: z >= 0
terms(z) -{ 2 }→ 1 + (1 + 0) + (1 + (1 + z)) :|: z >= 0, z = 0
terms(z) -{ 2 }→ 1 + (1 + (1 + z)) + (1 + (1 + z)) :|: z >= 0

Function symbols to be analyzed: {add}, {sqr}, {s}, {activate}
Previous analysis results are:

first: runtime: O(1) [1], size: O(n¹) [1 + z + z']
dbl: runtime: O(1) [1], size: O(n¹) [1 + z]
terms: runtime: O(1) [2], size: O(n¹) [5 + 2·z]

(37) IntTrsBoundProof (UPPER BOUND(ID) transformation)

Computed SIZE bound using CoFloCo for: add
after applying outer abstraction to obtain an ITS,
resulting in: O(n¹) with polynomial bound: 1 + z + z'

(38) Obligation:

Complexity RNTS consisting of the following rules:

activate(z) -{ 4 }→ s :|: s >= 0, s <= 1 * (1 + X) + 1, z - 2 >= 0, X >= 0, z - 2 = X
activate(z) -{ 1 }→ z :|: z >= 0
activate(z) -{ 2 }→ terms(terms(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ terms(sqr(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ terms(first(activate(X1''), activate(X2''))) :|: X1'' >= 0, z = 1 + (1 + X1'' + X2''), X2'' >= 0
activate(z) -{ 2 }→ terms(dbl(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ terms(add(activate(X1'), activate(X2'))) :|: z = 1 + (1 + X1' + X2'), X2' >= 0, X1' >= 0
activate(z) -{ 2 }→ sqr(terms(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ sqr(sqr(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ sqr(first(activate(X122), activate(X221))) :|: X122 >= 0, X221 >= 0, z = 1 + (1 + X122 + X221)
activate(z) -{ 2 }→ sqr(dbl(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ sqr(add(activate(X121), activate(X220))) :|: z = 1 + (1 + X121 + X220), X121 >= 0, X220 >= 0
activate(z) -{ 3 }→ sqr(1 + X) :|: z - 2 >= 0, X >= 0, z - 2 = X
activate(z) -{ 1 }→ first(activate(X1), activate(X2)) :|: X1 >= 0, X2 >= 0, z = 1 + X1 + X2
activate(z) -{ 2 }→ dbl(terms(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ dbl(sqr(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ dbl(first(activate(X124), activate(X223))) :|: X223 >= 0, X124 >= 0, z = 1 + (1 + X124 + X223)
activate(z) -{ 2 }→ dbl(dbl(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ dbl(add(activate(X123), activate(X222))) :|: z = 1 + (1 + X123 + X222), X222 >= 0, X123 >= 0
activate(z) -{ 1 }→ add(activate(X1), activate(X2)) :|: X1 >= 0, X2 >= 0, z = 1 + X1 + X2
activate(z) -{ 3 }→ 0 :|: z - 1 >= 0, z - 1 = 0
activate(z) -{ 3 }→ 1 + X' :|: z - 1 >= 0, X' >= 0, z - 1 = X'
activate(z) -{ 2 }→ 1 + X' :|: z - 1 >= 0, X' >= 0, z - 1 = X'
activate(z) -{ 4 }→ 1 + X' :|: z - 2 >= 0, X >= 0, z - 2 = X, X' >= 0, 1 + X = X'
activate(z) -{ 3 }→ 1 + (1 + sqr(N)) + (1 + (1 + N)) :|: z - 1 >= 0, z - 1 = N, N >= 0
activate(z) -{ 4 }→ 1 + (1 + sqr(N)) + (1 + (1 + N)) :|: z - 2 >= 0, X >= 0, z - 2 = X, 1 + X = N, N >= 0
add(z, z') -{ 1 }→ z' :|: z' >= 0, z = 0
add(z, z') -{ 1 }→ 1 + z + z' :|: z >= 0, z' >= 0
dbl(z) -{ 1 }→ 0 :|: z = 0
dbl(z) -{ 1 }→ 1 + z :|: z >= 0
first(z, z') -{ 1 }→ 1 :|: z' >= 0, z = 0
first(z, z') -{ 1 }→ 1 + z + z' :|: z >= 0, z' >= 0
s(z) -{ 1 }→ 1 + z :|: z >= 0
sqr(z) -{ 1 }→ 0 :|: z = 0
sqr(z) -{ 1 }→ 1 + z :|: z >= 0
terms(z) -{ 1 }→ 1 + z :|: z >= 0
terms(z) -{ 2 }→ 1 + (1 + 0) + (1 + (1 + z)) :|: z >= 0, z = 0
terms(z) -{ 2 }→ 1 + (1 + (1 + z)) + (1 + (1 + z)) :|: z >= 0

Function symbols to be analyzed: {add}, {sqr}, {s}, {activate}
Previous analysis results are:

first: runtime: O(1) [1], size: O(n¹) [1 + z + z']
dbl: runtime: O(1) [1], size: O(n¹) [1 + z]
terms: runtime: O(1) [2], size: O(n¹) [5 + 2·z]
add: runtime: ?, size: O(n¹) [1 + z + z']

(39) IntTrsBoundProof (UPPER BOUND(ID) transformation)

Computed RUNTIME bound using CoFloCo for: add
after applying outer abstraction to obtain an ITS,
resulting in: O(1) with polynomial bound: 1

(40) Obligation:

Complexity RNTS consisting of the following rules:

activate(z) -{ 4 }→ s :|: s >= 0, s <= 1 * (1 + X) + 1, z - 2 >= 0, X >= 0, z - 2 = X
activate(z) -{ 1 }→ z :|: z >= 0
activate(z) -{ 2 }→ terms(terms(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ terms(sqr(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ terms(first(activate(X1''), activate(X2''))) :|: X1'' >= 0, z = 1 + (1 + X1'' + X2''), X2'' >= 0
activate(z) -{ 2 }→ terms(dbl(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ terms(add(activate(X1'), activate(X2'))) :|: z = 1 + (1 + X1' + X2'), X2' >= 0, X1' >= 0
activate(z) -{ 2 }→ sqr(terms(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ sqr(sqr(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ sqr(first(activate(X122), activate(X221))) :|: X122 >= 0, X221 >= 0, z = 1 + (1 + X122 + X221)
activate(z) -{ 2 }→ sqr(dbl(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ sqr(add(activate(X121), activate(X220))) :|: z = 1 + (1 + X121 + X220), X121 >= 0, X220 >= 0
activate(z) -{ 3 }→ sqr(1 + X) :|: z - 2 >= 0, X >= 0, z - 2 = X
activate(z) -{ 1 }→ first(activate(X1), activate(X2)) :|: X1 >= 0, X2 >= 0, z = 1 + X1 + X2
activate(z) -{ 2 }→ dbl(terms(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ dbl(sqr(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ dbl(first(activate(X124), activate(X223))) :|: X223 >= 0, X124 >= 0, z = 1 + (1 + X124 + X223)
activate(z) -{ 2 }→ dbl(dbl(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ dbl(add(activate(X123), activate(X222))) :|: z = 1 + (1 + X123 + X222), X222 >= 0, X123 >= 0
activate(z) -{ 1 }→ add(activate(X1), activate(X2)) :|: X1 >= 0, X2 >= 0, z = 1 + X1 + X2
activate(z) -{ 3 }→ 0 :|: z - 1 >= 0, z - 1 = 0
activate(z) -{ 3 }→ 1 + X' :|: z - 1 >= 0, X' >= 0, z - 1 = X'
activate(z) -{ 2 }→ 1 + X' :|: z - 1 >= 0, X' >= 0, z - 1 = X'
activate(z) -{ 4 }→ 1 + X' :|: z - 2 >= 0, X >= 0, z - 2 = X, X' >= 0, 1 + X = X'
activate(z) -{ 3 }→ 1 + (1 + sqr(N)) + (1 + (1 + N)) :|: z - 1 >= 0, z - 1 = N, N >= 0
activate(z) -{ 4 }→ 1 + (1 + sqr(N)) + (1 + (1 + N)) :|: z - 2 >= 0, X >= 0, z - 2 = X, 1 + X = N, N >= 0
add(z, z') -{ 1 }→ z' :|: z' >= 0, z = 0
add(z, z') -{ 1 }→ 1 + z + z' :|: z >= 0, z' >= 0
dbl(z) -{ 1 }→ 0 :|: z = 0
dbl(z) -{ 1 }→ 1 + z :|: z >= 0
first(z, z') -{ 1 }→ 1 :|: z' >= 0, z = 0
first(z, z') -{ 1 }→ 1 + z + z' :|: z >= 0, z' >= 0
s(z) -{ 1 }→ 1 + z :|: z >= 0
sqr(z) -{ 1 }→ 0 :|: z = 0
sqr(z) -{ 1 }→ 1 + z :|: z >= 0
terms(z) -{ 1 }→ 1 + z :|: z >= 0
terms(z) -{ 2 }→ 1 + (1 + 0) + (1 + (1 + z)) :|: z >= 0, z = 0
terms(z) -{ 2 }→ 1 + (1 + (1 + z)) + (1 + (1 + z)) :|: z >= 0

Function symbols to be analyzed: {sqr}, {s}, {activate}
Previous analysis results are:

first: runtime: O(1) [1], size: O(n¹) [1 + z + z']
dbl: runtime: O(1) [1], size: O(n¹) [1 + z]
terms: runtime: O(1) [2], size: O(n¹) [5 + 2·z]
add: runtime: O(1) [1], size: O(n¹) [1 + z + z']

(41) ResultPropagationProof (UPPER BOUND(ID) transformation)

Applied inner abstraction using the recently inferred runtime/size bounds where possible.

(42) Obligation:

Complexity RNTS consisting of the following rules:

activate(z) -{ 4 }→ s :|: s >= 0, s <= 1 * (1 + X) + 1, z - 2 >= 0, X >= 0, z - 2 = X
activate(z) -{ 1 }→ z :|: z >= 0
activate(z) -{ 2 }→ terms(terms(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ terms(sqr(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ terms(first(activate(X1''), activate(X2''))) :|: X1'' >= 0, z = 1 + (1 + X1'' + X2''), X2'' >= 0
activate(z) -{ 2 }→ terms(dbl(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ terms(add(activate(X1'), activate(X2'))) :|: z = 1 + (1 + X1' + X2'), X2' >= 0, X1' >= 0
activate(z) -{ 2 }→ sqr(terms(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ sqr(sqr(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ sqr(first(activate(X122), activate(X221))) :|: X122 >= 0, X221 >= 0, z = 1 + (1 + X122 + X221)
activate(z) -{ 2 }→ sqr(dbl(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ sqr(add(activate(X121), activate(X220))) :|: z = 1 + (1 + X121 + X220), X121 >= 0, X220 >= 0
activate(z) -{ 3 }→ sqr(1 + X) :|: z - 2 >= 0, X >= 0, z - 2 = X
activate(z) -{ 1 }→ first(activate(X1), activate(X2)) :|: X1 >= 0, X2 >= 0, z = 1 + X1 + X2
activate(z) -{ 2 }→ dbl(terms(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ dbl(sqr(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ dbl(first(activate(X124), activate(X223))) :|: X223 >= 0, X124 >= 0, z = 1 + (1 + X124 + X223)
activate(z) -{ 2 }→ dbl(dbl(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ dbl(add(activate(X123), activate(X222))) :|: z = 1 + (1 + X123 + X222), X222 >= 0, X123 >= 0
activate(z) -{ 1 }→ add(activate(X1), activate(X2)) :|: X1 >= 0, X2 >= 0, z = 1 + X1 + X2
activate(z) -{ 3 }→ 0 :|: z - 1 >= 0, z - 1 = 0
activate(z) -{ 3 }→ 1 + X' :|: z - 1 >= 0, X' >= 0, z - 1 = X'
activate(z) -{ 2 }→ 1 + X' :|: z - 1 >= 0, X' >= 0, z - 1 = X'
activate(z) -{ 4 }→ 1 + X' :|: z - 2 >= 0, X >= 0, z - 2 = X, X' >= 0, 1 + X = X'
activate(z) -{ 3 }→ 1 + (1 + sqr(N)) + (1 + (1 + N)) :|: z - 1 >= 0, z - 1 = N, N >= 0
activate(z) -{ 4 }→ 1 + (1 + sqr(N)) + (1 + (1 + N)) :|: z - 2 >= 0, X >= 0, z - 2 = X, 1 + X = N, N >= 0
add(z, z') -{ 1 }→ z' :|: z' >= 0, z = 0
add(z, z') -{ 1 }→ 1 + z + z' :|: z >= 0, z' >= 0
dbl(z) -{ 1 }→ 0 :|: z = 0
dbl(z) -{ 1 }→ 1 + z :|: z >= 0
first(z, z') -{ 1 }→ 1 :|: z' >= 0, z = 0
first(z, z') -{ 1 }→ 1 + z + z' :|: z >= 0, z' >= 0
s(z) -{ 1 }→ 1 + z :|: z >= 0
sqr(z) -{ 1 }→ 0 :|: z = 0
sqr(z) -{ 1 }→ 1 + z :|: z >= 0
terms(z) -{ 1 }→ 1 + z :|: z >= 0
terms(z) -{ 2 }→ 1 + (1 + 0) + (1 + (1 + z)) :|: z >= 0, z = 0
terms(z) -{ 2 }→ 1 + (1 + (1 + z)) + (1 + (1 + z)) :|: z >= 0

Function symbols to be analyzed: {sqr}, {s}, {activate}
Previous analysis results are:

first: runtime: O(1) [1], size: O(n¹) [1 + z + z']
dbl: runtime: O(1) [1], size: O(n¹) [1 + z]
terms: runtime: O(1) [2], size: O(n¹) [5 + 2·z]
add: runtime: O(1) [1], size: O(n¹) [1 + z + z']

(43) IntTrsBoundProof (UPPER BOUND(ID) transformation)

Computed SIZE bound using CoFloCo for: sqr
after applying outer abstraction to obtain an ITS,
resulting in: O(n¹) with polynomial bound: 1 + z

(44) Obligation:

Complexity RNTS consisting of the following rules:

activate(z) -{ 4 }→ s :|: s >= 0, s <= 1 * (1 + X) + 1, z - 2 >= 0, X >= 0, z - 2 = X
activate(z) -{ 1 }→ z :|: z >= 0
activate(z) -{ 2 }→ terms(terms(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ terms(sqr(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ terms(first(activate(X1''), activate(X2''))) :|: X1'' >= 0, z = 1 + (1 + X1'' + X2''), X2'' >= 0
activate(z) -{ 2 }→ terms(dbl(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ terms(add(activate(X1'), activate(X2'))) :|: z = 1 + (1 + X1' + X2'), X2' >= 0, X1' >= 0
activate(z) -{ 2 }→ sqr(terms(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ sqr(sqr(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ sqr(first(activate(X122), activate(X221))) :|: X122 >= 0, X221 >= 0, z = 1 + (1 + X122 + X221)
activate(z) -{ 2 }→ sqr(dbl(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ sqr(add(activate(X121), activate(X220))) :|: z = 1 + (1 + X121 + X220), X121 >= 0, X220 >= 0
activate(z) -{ 3 }→ sqr(1 + X) :|: z - 2 >= 0, X >= 0, z - 2 = X
activate(z) -{ 1 }→ first(activate(X1), activate(X2)) :|: X1 >= 0, X2 >= 0, z = 1 + X1 + X2
activate(z) -{ 2 }→ dbl(terms(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ dbl(sqr(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ dbl(first(activate(X124), activate(X223))) :|: X223 >= 0, X124 >= 0, z = 1 + (1 + X124 + X223)
activate(z) -{ 2 }→ dbl(dbl(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ dbl(add(activate(X123), activate(X222))) :|: z = 1 + (1 + X123 + X222), X222 >= 0, X123 >= 0
activate(z) -{ 1 }→ add(activate(X1), activate(X2)) :|: X1 >= 0, X2 >= 0, z = 1 + X1 + X2
activate(z) -{ 3 }→ 0 :|: z - 1 >= 0, z - 1 = 0
activate(z) -{ 3 }→ 1 + X' :|: z - 1 >= 0, X' >= 0, z - 1 = X'
activate(z) -{ 2 }→ 1 + X' :|: z - 1 >= 0, X' >= 0, z - 1 = X'
activate(z) -{ 4 }→ 1 + X' :|: z - 2 >= 0, X >= 0, z - 2 = X, X' >= 0, 1 + X = X'
activate(z) -{ 3 }→ 1 + (1 + sqr(N)) + (1 + (1 + N)) :|: z - 1 >= 0, z - 1 = N, N >= 0
activate(z) -{ 4 }→ 1 + (1 + sqr(N)) + (1 + (1 + N)) :|: z - 2 >= 0, X >= 0, z - 2 = X, 1 + X = N, N >= 0
add(z, z') -{ 1 }→ z' :|: z' >= 0, z = 0
add(z, z') -{ 1 }→ 1 + z + z' :|: z >= 0, z' >= 0
dbl(z) -{ 1 }→ 0 :|: z = 0
dbl(z) -{ 1 }→ 1 + z :|: z >= 0
first(z, z') -{ 1 }→ 1 :|: z' >= 0, z = 0
first(z, z') -{ 1 }→ 1 + z + z' :|: z >= 0, z' >= 0
s(z) -{ 1 }→ 1 + z :|: z >= 0
sqr(z) -{ 1 }→ 0 :|: z = 0
sqr(z) -{ 1 }→ 1 + z :|: z >= 0
terms(z) -{ 1 }→ 1 + z :|: z >= 0
terms(z) -{ 2 }→ 1 + (1 + 0) + (1 + (1 + z)) :|: z >= 0, z = 0
terms(z) -{ 2 }→ 1 + (1 + (1 + z)) + (1 + (1 + z)) :|: z >= 0

Function symbols to be analyzed: {sqr}, {s}, {activate}
Previous analysis results are:

(45) IntTrsBoundProof (UPPER BOUND(ID) transformation)

Computed RUNTIME bound using CoFloCo for: sqr
after applying outer abstraction to obtain an ITS,
resulting in: O(1) with polynomial bound: 1

(46) Obligation:

Complexity RNTS consisting of the following rules:

activate(z) -{ 4 }→ s :|: s >= 0, s <= 1 * (1 + X) + 1, z - 2 >= 0, X >= 0, z - 2 = X
activate(z) -{ 1 }→ z :|: z >= 0
activate(z) -{ 2 }→ terms(terms(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ terms(sqr(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ terms(first(activate(X1''), activate(X2''))) :|: X1'' >= 0, z = 1 + (1 + X1'' + X2''), X2'' >= 0
activate(z) -{ 2 }→ terms(dbl(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ terms(add(activate(X1'), activate(X2'))) :|: z = 1 + (1 + X1' + X2'), X2' >= 0, X1' >= 0
activate(z) -{ 2 }→ sqr(terms(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ sqr(sqr(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ sqr(first(activate(X122), activate(X221))) :|: X122 >= 0, X221 >= 0, z = 1 + (1 + X122 + X221)
activate(z) -{ 2 }→ sqr(dbl(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ sqr(add(activate(X121), activate(X220))) :|: z = 1 + (1 + X121 + X220), X121 >= 0, X220 >= 0
activate(z) -{ 3 }→ sqr(1 + X) :|: z - 2 >= 0, X >= 0, z - 2 = X
activate(z) -{ 1 }→ first(activate(X1), activate(X2)) :|: X1 >= 0, X2 >= 0, z = 1 + X1 + X2
activate(z) -{ 2 }→ dbl(terms(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ dbl(sqr(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ dbl(first(activate(X124), activate(X223))) :|: X223 >= 0, X124 >= 0, z = 1 + (1 + X124 + X223)
activate(z) -{ 2 }→ dbl(dbl(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ dbl(add(activate(X123), activate(X222))) :|: z = 1 + (1 + X123 + X222), X222 >= 0, X123 >= 0
activate(z) -{ 1 }→ add(activate(X1), activate(X2)) :|: X1 >= 0, X2 >= 0, z = 1 + X1 + X2
activate(z) -{ 3 }→ 0 :|: z - 1 >= 0, z - 1 = 0
activate(z) -{ 3 }→ 1 + X' :|: z - 1 >= 0, X' >= 0, z - 1 = X'
activate(z) -{ 2 }→ 1 + X' :|: z - 1 >= 0, X' >= 0, z - 1 = X'
activate(z) -{ 4 }→ 1 + X' :|: z - 2 >= 0, X >= 0, z - 2 = X, X' >= 0, 1 + X = X'
activate(z) -{ 3 }→ 1 + (1 + sqr(N)) + (1 + (1 + N)) :|: z - 1 >= 0, z - 1 = N, N >= 0
activate(z) -{ 4 }→ 1 + (1 + sqr(N)) + (1 + (1 + N)) :|: z - 2 >= 0, X >= 0, z - 2 = X, 1 + X = N, N >= 0
add(z, z') -{ 1 }→ z' :|: z' >= 0, z = 0
add(z, z') -{ 1 }→ 1 + z + z' :|: z >= 0, z' >= 0
dbl(z) -{ 1 }→ 0 :|: z = 0
dbl(z) -{ 1 }→ 1 + z :|: z >= 0
first(z, z') -{ 1 }→ 1 :|: z' >= 0, z = 0
first(z, z') -{ 1 }→ 1 + z + z' :|: z >= 0, z' >= 0
s(z) -{ 1 }→ 1 + z :|: z >= 0
sqr(z) -{ 1 }→ 0 :|: z = 0
sqr(z) -{ 1 }→ 1 + z :|: z >= 0
terms(z) -{ 1 }→ 1 + z :|: z >= 0
terms(z) -{ 2 }→ 1 + (1 + 0) + (1 + (1 + z)) :|: z >= 0, z = 0
terms(z) -{ 2 }→ 1 + (1 + (1 + z)) + (1 + (1 + z)) :|: z >= 0

Function symbols to be analyzed: {s}, {activate}
Previous analysis results are:

first: runtime: O(1) [1], size: O(n¹) [1 + z + z']
dbl: runtime: O(1) [1], size: O(n¹) [1 + z]
terms: runtime: O(1) [2], size: O(n¹) [5 + 2·z]
add: runtime: O(1) [1], size: O(n¹) [1 + z + z']
sqr: runtime: O(1) [1], size: O(n¹) [1 + z]

(47) ResultPropagationProof (UPPER BOUND(ID) transformation)

Applied inner abstraction using the recently inferred runtime/size bounds where possible.

(48) Obligation:

Complexity RNTS consisting of the following rules:

activate(z) -{ 4 }→ s :|: s >= 0, s <= 1 * (1 + X) + 1, z - 2 >= 0, X >= 0, z - 2 = X
activate(z) -{ 4 }→ s' :|: s' >= 0, s' <= 1 * (1 + X) + 1, z - 2 >= 0, X >= 0, z - 2 = X
activate(z) -{ 1 }→ z :|: z >= 0
activate(z) -{ 2 }→ terms(terms(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ terms(sqr(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ terms(first(activate(X1''), activate(X2''))) :|: X1'' >= 0, z = 1 + (1 + X1'' + X2''), X2'' >= 0
activate(z) -{ 2 }→ terms(dbl(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ terms(add(activate(X1'), activate(X2'))) :|: z = 1 + (1 + X1' + X2'), X2' >= 0, X1' >= 0
activate(z) -{ 2 }→ sqr(terms(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ sqr(sqr(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ sqr(first(activate(X122), activate(X221))) :|: X122 >= 0, X221 >= 0, z = 1 + (1 + X122 + X221)
activate(z) -{ 2 }→ sqr(dbl(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ sqr(add(activate(X121), activate(X220))) :|: z = 1 + (1 + X121 + X220), X121 >= 0, X220 >= 0
activate(z) -{ 1 }→ first(activate(X1), activate(X2)) :|: X1 >= 0, X2 >= 0, z = 1 + X1 + X2
activate(z) -{ 2 }→ dbl(terms(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ dbl(sqr(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ dbl(first(activate(X124), activate(X223))) :|: X223 >= 0, X124 >= 0, z = 1 + (1 + X124 + X223)
activate(z) -{ 2 }→ dbl(dbl(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ dbl(add(activate(X123), activate(X222))) :|: z = 1 + (1 + X123 + X222), X222 >= 0, X123 >= 0
activate(z) -{ 1 }→ add(activate(X1), activate(X2)) :|: X1 >= 0, X2 >= 0, z = 1 + X1 + X2
activate(z) -{ 3 }→ 0 :|: z - 1 >= 0, z - 1 = 0
activate(z) -{ 3 }→ 1 + X' :|: z - 1 >= 0, X' >= 0, z - 1 = X'
activate(z) -{ 2 }→ 1 + X' :|: z - 1 >= 0, X' >= 0, z - 1 = X'
activate(z) -{ 4 }→ 1 + X' :|: z - 2 >= 0, X >= 0, z - 2 = X, X' >= 0, 1 + X = X'
activate(z) -{ 4 }→ 1 + (1 + s'') + (1 + (1 + N)) :|: s'' >= 0, s'' <= 1 * N + 1, z - 1 >= 0, z - 1 = N, N >= 0
activate(z) -{ 5 }→ 1 + (1 + s1) + (1 + (1 + N)) :|: s1 >= 0, s1 <= 1 * N + 1, z - 2 >= 0, X >= 0, z - 2 = X, 1 + X = N, N >= 0
add(z, z') -{ 1 }→ z' :|: z' >= 0, z = 0
add(z, z') -{ 1 }→ 1 + z + z' :|: z >= 0, z' >= 0
dbl(z) -{ 1 }→ 0 :|: z = 0
dbl(z) -{ 1 }→ 1 + z :|: z >= 0
first(z, z') -{ 1 }→ 1 :|: z' >= 0, z = 0
first(z, z') -{ 1 }→ 1 + z + z' :|: z >= 0, z' >= 0
s(z) -{ 1 }→ 1 + z :|: z >= 0
sqr(z) -{ 1 }→ 0 :|: z = 0
sqr(z) -{ 1 }→ 1 + z :|: z >= 0
terms(z) -{ 1 }→ 1 + z :|: z >= 0
terms(z) -{ 2 }→ 1 + (1 + 0) + (1 + (1 + z)) :|: z >= 0, z = 0
terms(z) -{ 2 }→ 1 + (1 + (1 + z)) + (1 + (1 + z)) :|: z >= 0

Function symbols to be analyzed: {s}, {activate}
Previous analysis results are:

(49) IntTrsBoundProof (UPPER BOUND(ID) transformation)

Computed SIZE bound using CoFloCo for: s
after applying outer abstraction to obtain an ITS,
resulting in: O(n¹) with polynomial bound: 1 + z

(50) Obligation:

Complexity RNTS consisting of the following rules:

activate(z) -{ 4 }→ s :|: s >= 0, s <= 1 * (1 + X) + 1, z - 2 >= 0, X >= 0, z - 2 = X
activate(z) -{ 4 }→ s' :|: s' >= 0, s' <= 1 * (1 + X) + 1, z - 2 >= 0, X >= 0, z - 2 = X
activate(z) -{ 1 }→ z :|: z >= 0
activate(z) -{ 2 }→ terms(terms(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ terms(sqr(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ terms(first(activate(X1''), activate(X2''))) :|: X1'' >= 0, z = 1 + (1 + X1'' + X2''), X2'' >= 0
activate(z) -{ 2 }→ terms(dbl(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ terms(add(activate(X1'), activate(X2'))) :|: z = 1 + (1 + X1' + X2'), X2' >= 0, X1' >= 0
activate(z) -{ 2 }→ sqr(terms(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ sqr(sqr(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ sqr(first(activate(X122), activate(X221))) :|: X122 >= 0, X221 >= 0, z = 1 + (1 + X122 + X221)
activate(z) -{ 2 }→ sqr(dbl(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ sqr(add(activate(X121), activate(X220))) :|: z = 1 + (1 + X121 + X220), X121 >= 0, X220 >= 0
activate(z) -{ 1 }→ first(activate(X1), activate(X2)) :|: X1 >= 0, X2 >= 0, z = 1 + X1 + X2
activate(z) -{ 2 }→ dbl(terms(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ dbl(sqr(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ dbl(first(activate(X124), activate(X223))) :|: X223 >= 0, X124 >= 0, z = 1 + (1 + X124 + X223)
activate(z) -{ 2 }→ dbl(dbl(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ dbl(add(activate(X123), activate(X222))) :|: z = 1 + (1 + X123 + X222), X222 >= 0, X123 >= 0
activate(z) -{ 1 }→ add(activate(X1), activate(X2)) :|: X1 >= 0, X2 >= 0, z = 1 + X1 + X2
activate(z) -{ 3 }→ 0 :|: z - 1 >= 0, z - 1 = 0
activate(z) -{ 3 }→ 1 + X' :|: z - 1 >= 0, X' >= 0, z - 1 = X'
activate(z) -{ 2 }→ 1 + X' :|: z - 1 >= 0, X' >= 0, z - 1 = X'
activate(z) -{ 4 }→ 1 + X' :|: z - 2 >= 0, X >= 0, z - 2 = X, X' >= 0, 1 + X = X'
activate(z) -{ 4 }→ 1 + (1 + s'') + (1 + (1 + N)) :|: s'' >= 0, s'' <= 1 * N + 1, z - 1 >= 0, z - 1 = N, N >= 0
activate(z) -{ 5 }→ 1 + (1 + s1) + (1 + (1 + N)) :|: s1 >= 0, s1 <= 1 * N + 1, z - 2 >= 0, X >= 0, z - 2 = X, 1 + X = N, N >= 0
add(z, z') -{ 1 }→ z' :|: z' >= 0, z = 0
add(z, z') -{ 1 }→ 1 + z + z' :|: z >= 0, z' >= 0
dbl(z) -{ 1 }→ 0 :|: z = 0
dbl(z) -{ 1 }→ 1 + z :|: z >= 0
first(z, z') -{ 1 }→ 1 :|: z' >= 0, z = 0
first(z, z') -{ 1 }→ 1 + z + z' :|: z >= 0, z' >= 0
s(z) -{ 1 }→ 1 + z :|: z >= 0
sqr(z) -{ 1 }→ 0 :|: z = 0
sqr(z) -{ 1 }→ 1 + z :|: z >= 0
terms(z) -{ 1 }→ 1 + z :|: z >= 0
terms(z) -{ 2 }→ 1 + (1 + 0) + (1 + (1 + z)) :|: z >= 0, z = 0
terms(z) -{ 2 }→ 1 + (1 + (1 + z)) + (1 + (1 + z)) :|: z >= 0

Function symbols to be analyzed: {s}, {activate}
Previous analysis results are:

(51) IntTrsBoundProof (UPPER BOUND(ID) transformation)

Computed RUNTIME bound using CoFloCo for: s
after applying outer abstraction to obtain an ITS,
resulting in: O(1) with polynomial bound: 1

(52) Obligation:

Complexity RNTS consisting of the following rules:

activate(z) -{ 4 }→ s :|: s >= 0, s <= 1 * (1 + X) + 1, z - 2 >= 0, X >= 0, z - 2 = X
activate(z) -{ 4 }→ s' :|: s' >= 0, s' <= 1 * (1 + X) + 1, z - 2 >= 0, X >= 0, z - 2 = X
activate(z) -{ 1 }→ z :|: z >= 0
activate(z) -{ 2 }→ terms(terms(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ terms(sqr(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ terms(first(activate(X1''), activate(X2''))) :|: X1'' >= 0, z = 1 + (1 + X1'' + X2''), X2'' >= 0
activate(z) -{ 2 }→ terms(dbl(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ terms(add(activate(X1'), activate(X2'))) :|: z = 1 + (1 + X1' + X2'), X2' >= 0, X1' >= 0
activate(z) -{ 2 }→ sqr(terms(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ sqr(sqr(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ sqr(first(activate(X122), activate(X221))) :|: X122 >= 0, X221 >= 0, z = 1 + (1 + X122 + X221)
activate(z) -{ 2 }→ sqr(dbl(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ sqr(add(activate(X121), activate(X220))) :|: z = 1 + (1 + X121 + X220), X121 >= 0, X220 >= 0
activate(z) -{ 1 }→ first(activate(X1), activate(X2)) :|: X1 >= 0, X2 >= 0, z = 1 + X1 + X2
activate(z) -{ 2 }→ dbl(terms(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ dbl(sqr(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ dbl(first(activate(X124), activate(X223))) :|: X223 >= 0, X124 >= 0, z = 1 + (1 + X124 + X223)
activate(z) -{ 2 }→ dbl(dbl(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ dbl(add(activate(X123), activate(X222))) :|: z = 1 + (1 + X123 + X222), X222 >= 0, X123 >= 0
activate(z) -{ 1 }→ add(activate(X1), activate(X2)) :|: X1 >= 0, X2 >= 0, z = 1 + X1 + X2
activate(z) -{ 3 }→ 0 :|: z - 1 >= 0, z - 1 = 0
activate(z) -{ 3 }→ 1 + X' :|: z - 1 >= 0, X' >= 0, z - 1 = X'
activate(z) -{ 2 }→ 1 + X' :|: z - 1 >= 0, X' >= 0, z - 1 = X'
activate(z) -{ 4 }→ 1 + X' :|: z - 2 >= 0, X >= 0, z - 2 = X, X' >= 0, 1 + X = X'
activate(z) -{ 4 }→ 1 + (1 + s'') + (1 + (1 + N)) :|: s'' >= 0, s'' <= 1 * N + 1, z - 1 >= 0, z - 1 = N, N >= 0
activate(z) -{ 5 }→ 1 + (1 + s1) + (1 + (1 + N)) :|: s1 >= 0, s1 <= 1 * N + 1, z - 2 >= 0, X >= 0, z - 2 = X, 1 + X = N, N >= 0
add(z, z') -{ 1 }→ z' :|: z' >= 0, z = 0
add(z, z') -{ 1 }→ 1 + z + z' :|: z >= 0, z' >= 0
dbl(z) -{ 1 }→ 0 :|: z = 0
dbl(z) -{ 1 }→ 1 + z :|: z >= 0
first(z, z') -{ 1 }→ 1 :|: z' >= 0, z = 0
first(z, z') -{ 1 }→ 1 + z + z' :|: z >= 0, z' >= 0
s(z) -{ 1 }→ 1 + z :|: z >= 0
sqr(z) -{ 1 }→ 0 :|: z = 0
sqr(z) -{ 1 }→ 1 + z :|: z >= 0
terms(z) -{ 1 }→ 1 + z :|: z >= 0
terms(z) -{ 2 }→ 1 + (1 + 0) + (1 + (1 + z)) :|: z >= 0, z = 0
terms(z) -{ 2 }→ 1 + (1 + (1 + z)) + (1 + (1 + z)) :|: z >= 0

Function symbols to be analyzed: {activate}
Previous analysis results are:

(53) ResultPropagationProof (UPPER BOUND(ID) transformation)

Applied inner abstraction using the recently inferred runtime/size bounds where possible.

(54) Obligation:

Complexity RNTS consisting of the following rules:

activate(z) -{ 4 }→ s :|: s >= 0, s <= 1 * (1 + X) + 1, z - 2 >= 0, X >= 0, z - 2 = X
activate(z) -{ 4 }→ s' :|: s' >= 0, s' <= 1 * (1 + X) + 1, z - 2 >= 0, X >= 0, z - 2 = X
activate(z) -{ 1 }→ z :|: z >= 0
activate(z) -{ 2 }→ terms(terms(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ terms(sqr(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ terms(first(activate(X1''), activate(X2''))) :|: X1'' >= 0, z = 1 + (1 + X1'' + X2''), X2'' >= 0
activate(z) -{ 2 }→ terms(dbl(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ terms(add(activate(X1'), activate(X2'))) :|: z = 1 + (1 + X1' + X2'), X2' >= 0, X1' >= 0
activate(z) -{ 2 }→ sqr(terms(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ sqr(sqr(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ sqr(first(activate(X122), activate(X221))) :|: X122 >= 0, X221 >= 0, z = 1 + (1 + X122 + X221)
activate(z) -{ 2 }→ sqr(dbl(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ sqr(add(activate(X121), activate(X220))) :|: z = 1 + (1 + X121 + X220), X121 >= 0, X220 >= 0
activate(z) -{ 1 }→ first(activate(X1), activate(X2)) :|: X1 >= 0, X2 >= 0, z = 1 + X1 + X2
activate(z) -{ 2 }→ dbl(terms(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ dbl(sqr(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ dbl(first(activate(X124), activate(X223))) :|: X223 >= 0, X124 >= 0, z = 1 + (1 + X124 + X223)
activate(z) -{ 2 }→ dbl(dbl(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ dbl(add(activate(X123), activate(X222))) :|: z = 1 + (1 + X123 + X222), X222 >= 0, X123 >= 0
activate(z) -{ 1 }→ add(activate(X1), activate(X2)) :|: X1 >= 0, X2 >= 0, z = 1 + X1 + X2
activate(z) -{ 3 }→ 0 :|: z - 1 >= 0, z - 1 = 0
activate(z) -{ 3 }→ 1 + X' :|: z - 1 >= 0, X' >= 0, z - 1 = X'
activate(z) -{ 2 }→ 1 + X' :|: z - 1 >= 0, X' >= 0, z - 1 = X'
activate(z) -{ 4 }→ 1 + X' :|: z - 2 >= 0, X >= 0, z - 2 = X, X' >= 0, 1 + X = X'
activate(z) -{ 4 }→ 1 + (1 + s'') + (1 + (1 + N)) :|: s'' >= 0, s'' <= 1 * N + 1, z - 1 >= 0, z - 1 = N, N >= 0
activate(z) -{ 5 }→ 1 + (1 + s1) + (1 + (1 + N)) :|: s1 >= 0, s1 <= 1 * N + 1, z - 2 >= 0, X >= 0, z - 2 = X, 1 + X = N, N >= 0
add(z, z') -{ 1 }→ z' :|: z' >= 0, z = 0
add(z, z') -{ 1 }→ 1 + z + z' :|: z >= 0, z' >= 0
dbl(z) -{ 1 }→ 0 :|: z = 0
dbl(z) -{ 1 }→ 1 + z :|: z >= 0
first(z, z') -{ 1 }→ 1 :|: z' >= 0, z = 0
first(z, z') -{ 1 }→ 1 + z + z' :|: z >= 0, z' >= 0
s(z) -{ 1 }→ 1 + z :|: z >= 0
sqr(z) -{ 1 }→ 0 :|: z = 0
sqr(z) -{ 1 }→ 1 + z :|: z >= 0
terms(z) -{ 1 }→ 1 + z :|: z >= 0
terms(z) -{ 2 }→ 1 + (1 + 0) + (1 + (1 + z)) :|: z >= 0, z = 0
terms(z) -{ 2 }→ 1 + (1 + (1 + z)) + (1 + (1 + z)) :|: z >= 0

Function symbols to be analyzed: {activate}
Previous analysis results are:

(55) IntTrsBoundProof (UPPER BOUND(ID) transformation)

Computed SIZE bound using KoAT for: activate
after applying outer abstraction to obtain an ITS,
resulting in: EXP with polynomial bound: ?

(56) Obligation:

Complexity RNTS consisting of the following rules:

activate(z) -{ 4 }→ s :|: s >= 0, s <= 1 * (1 + X) + 1, z - 2 >= 0, X >= 0, z - 2 = X
activate(z) -{ 4 }→ s' :|: s' >= 0, s' <= 1 * (1 + X) + 1, z - 2 >= 0, X >= 0, z - 2 = X
activate(z) -{ 1 }→ z :|: z >= 0
activate(z) -{ 2 }→ terms(terms(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ terms(sqr(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ terms(first(activate(X1''), activate(X2''))) :|: X1'' >= 0, z = 1 + (1 + X1'' + X2''), X2'' >= 0
activate(z) -{ 2 }→ terms(dbl(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ terms(add(activate(X1'), activate(X2'))) :|: z = 1 + (1 + X1' + X2'), X2' >= 0, X1' >= 0
activate(z) -{ 2 }→ sqr(terms(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ sqr(sqr(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ sqr(first(activate(X122), activate(X221))) :|: X122 >= 0, X221 >= 0, z = 1 + (1 + X122 + X221)
activate(z) -{ 2 }→ sqr(dbl(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ sqr(add(activate(X121), activate(X220))) :|: z = 1 + (1 + X121 + X220), X121 >= 0, X220 >= 0
activate(z) -{ 1 }→ first(activate(X1), activate(X2)) :|: X1 >= 0, X2 >= 0, z = 1 + X1 + X2
activate(z) -{ 2 }→ dbl(terms(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ dbl(sqr(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ dbl(first(activate(X124), activate(X223))) :|: X223 >= 0, X124 >= 0, z = 1 + (1 + X124 + X223)
activate(z) -{ 2 }→ dbl(dbl(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ dbl(add(activate(X123), activate(X222))) :|: z = 1 + (1 + X123 + X222), X222 >= 0, X123 >= 0
activate(z) -{ 1 }→ add(activate(X1), activate(X2)) :|: X1 >= 0, X2 >= 0, z = 1 + X1 + X2
activate(z) -{ 3 }→ 0 :|: z - 1 >= 0, z - 1 = 0
activate(z) -{ 3 }→ 1 + X' :|: z - 1 >= 0, X' >= 0, z - 1 = X'
activate(z) -{ 2 }→ 1 + X' :|: z - 1 >= 0, X' >= 0, z - 1 = X'
activate(z) -{ 4 }→ 1 + X' :|: z - 2 >= 0, X >= 0, z - 2 = X, X' >= 0, 1 + X = X'
activate(z) -{ 4 }→ 1 + (1 + s'') + (1 + (1 + N)) :|: s'' >= 0, s'' <= 1 * N + 1, z - 1 >= 0, z - 1 = N, N >= 0
activate(z) -{ 5 }→ 1 + (1 + s1) + (1 + (1 + N)) :|: s1 >= 0, s1 <= 1 * N + 1, z - 2 >= 0, X >= 0, z - 2 = X, 1 + X = N, N >= 0
add(z, z') -{ 1 }→ z' :|: z' >= 0, z = 0
add(z, z') -{ 1 }→ 1 + z + z' :|: z >= 0, z' >= 0
dbl(z) -{ 1 }→ 0 :|: z = 0
dbl(z) -{ 1 }→ 1 + z :|: z >= 0
first(z, z') -{ 1 }→ 1 :|: z' >= 0, z = 0
first(z, z') -{ 1 }→ 1 + z + z' :|: z >= 0, z' >= 0
s(z) -{ 1 }→ 1 + z :|: z >= 0
sqr(z) -{ 1 }→ 0 :|: z = 0
sqr(z) -{ 1 }→ 1 + z :|: z >= 0
terms(z) -{ 1 }→ 1 + z :|: z >= 0
terms(z) -{ 2 }→ 1 + (1 + 0) + (1 + (1 + z)) :|: z >= 0, z = 0
terms(z) -{ 2 }→ 1 + (1 + (1 + z)) + (1 + (1 + z)) :|: z >= 0

Function symbols to be analyzed: {activate}
Previous analysis results are:

(57) IntTrsBoundProof (UPPER BOUND(ID) transformation)

Computed RUNTIME bound using KoAT for: activate
after applying outer abstraction to obtain an ITS,
resulting in: O(n¹) with polynomial bound: 73 + 146·z

(58) Obligation:

Complexity RNTS consisting of the following rules:

activate(z) -{ 4 }→ s :|: s >= 0, s <= 1 * (1 + X) + 1, z - 2 >= 0, X >= 0, z - 2 = X
activate(z) -{ 4 }→ s' :|: s' >= 0, s' <= 1 * (1 + X) + 1, z - 2 >= 0, X >= 0, z - 2 = X
activate(z) -{ 1 }→ z :|: z >= 0
activate(z) -{ 2 }→ terms(terms(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ terms(sqr(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ terms(first(activate(X1''), activate(X2''))) :|: X1'' >= 0, z = 1 + (1 + X1'' + X2''), X2'' >= 0
activate(z) -{ 2 }→ terms(dbl(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ terms(add(activate(X1'), activate(X2'))) :|: z = 1 + (1 + X1' + X2'), X2' >= 0, X1' >= 0
activate(z) -{ 2 }→ sqr(terms(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ sqr(sqr(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ sqr(first(activate(X122), activate(X221))) :|: X122 >= 0, X221 >= 0, z = 1 + (1 + X122 + X221)
activate(z) -{ 2 }→ sqr(dbl(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ sqr(add(activate(X121), activate(X220))) :|: z = 1 + (1 + X121 + X220), X121 >= 0, X220 >= 0
activate(z) -{ 1 }→ first(activate(X1), activate(X2)) :|: X1 >= 0, X2 >= 0, z = 1 + X1 + X2
activate(z) -{ 2 }→ dbl(terms(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ dbl(sqr(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ dbl(first(activate(X124), activate(X223))) :|: X223 >= 0, X124 >= 0, z = 1 + (1 + X124 + X223)
activate(z) -{ 2 }→ dbl(dbl(activate(z - 2))) :|: z - 2 >= 0
activate(z) -{ 2 }→ dbl(add(activate(X123), activate(X222))) :|: z = 1 + (1 + X123 + X222), X222 >= 0, X123 >= 0
activate(z) -{ 1 }→ add(activate(X1), activate(X2)) :|: X1 >= 0, X2 >= 0, z = 1 + X1 + X2
activate(z) -{ 3 }→ 0 :|: z - 1 >= 0, z - 1 = 0
activate(z) -{ 3 }→ 1 + X' :|: z - 1 >= 0, X' >= 0, z - 1 = X'
activate(z) -{ 2 }→ 1 + X' :|: z - 1 >= 0, X' >= 0, z - 1 = X'
activate(z) -{ 4 }→ 1 + X' :|: z - 2 >= 0, X >= 0, z - 2 = X, X' >= 0, 1 + X = X'
activate(z) -{ 4 }→ 1 + (1 + s'') + (1 + (1 + N)) :|: s'' >= 0, s'' <= 1 * N + 1, z - 1 >= 0, z - 1 = N, N >= 0
activate(z) -{ 5 }→ 1 + (1 + s1) + (1 + (1 + N)) :|: s1 >= 0, s1 <= 1 * N + 1, z - 2 >= 0, X >= 0, z - 2 = X, 1 + X = N, N >= 0
add(z, z') -{ 1 }→ z' :|: z' >= 0, z = 0
add(z, z') -{ 1 }→ 1 + z + z' :|: z >= 0, z' >= 0
dbl(z) -{ 1 }→ 0 :|: z = 0
dbl(z) -{ 1 }→ 1 + z :|: z >= 0
first(z, z') -{ 1 }→ 1 :|: z' >= 0, z = 0
first(z, z') -{ 1 }→ 1 + z + z' :|: z >= 0, z' >= 0
s(z) -{ 1 }→ 1 + z :|: z >= 0
sqr(z) -{ 1 }→ 0 :|: z = 0
sqr(z) -{ 1 }→ 1 + z :|: z >= 0
terms(z) -{ 1 }→ 1 + z :|: z >= 0
terms(z) -{ 2 }→ 1 + (1 + 0) + (1 + (1 + z)) :|: z >= 0, z = 0
terms(z) -{ 2 }→ 1 + (1 + (1 + z)) + (1 + (1 + z)) :|: z >= 0

Function symbols to be analyzed:
Previous analysis results are:

(59) FinalProof (EQUIVALENT transformation)

Computed overall runtime complexity

(0) Obligation:

(1) TrsToWeightedTrsProof (BOTH BOUNDS(ID, ID) transformation)

(2) Obligation:

(3) InnermostUnusableRulesProof (BOTH BOUNDS(ID, ID) transformation)

(4) Obligation:

(5) TypeInferenceProof (BOTH BOUNDS(ID, ID) transformation)

(6) Obligation:

(7) CompletionProof (UPPER BOUND(ID) transformation)

(8) Obligation:

(9) NarrowingProof (BOTH BOUNDS(ID, ID) transformation)

(10) Obligation:

(11) CpxTypedWeightedTrsToRntsProof (UPPER BOUND(ID) transformation)

(12) Obligation:

(13) InliningProof (UPPER BOUND(ID) transformation)

(14) Obligation:

(15) SimplificationProof (BOTH BOUNDS(ID, ID) transformation)

(16) Obligation:

(17) CpxRntsAnalysisOrderProof (BOTH BOUNDS(ID, ID) transformation)

(18) Obligation:

(19) IntTrsBoundProof (UPPER BOUND(ID) transformation)

(20) Obligation:

(21) IntTrsBoundProof (UPPER BOUND(ID) transformation)

(22) Obligation:

(23) ResultPropagationProof (UPPER BOUND(ID) transformation)

(24) Obligation:

(25) IntTrsBoundProof (UPPER BOUND(ID) transformation)

(26) Obligation:

(27) IntTrsBoundProof (UPPER BOUND(ID) transformation)

(28) Obligation:

(29) ResultPropagationProof (UPPER BOUND(ID) transformation)

(30) Obligation:

(31) IntTrsBoundProof (UPPER BOUND(ID) transformation)

(32) Obligation:

(33) IntTrsBoundProof (UPPER BOUND(ID) transformation)

(34) Obligation:

(35) ResultPropagationProof (UPPER BOUND(ID) transformation)

(36) Obligation:

(37) IntTrsBoundProof (UPPER BOUND(ID) transformation)

(38) Obligation:

(39) IntTrsBoundProof (UPPER BOUND(ID) transformation)

(40) Obligation:

(41) ResultPropagationProof (UPPER BOUND(ID) transformation)

(42) Obligation:

(43) IntTrsBoundProof (UPPER BOUND(ID) transformation)

(44) Obligation:

(45) IntTrsBoundProof (UPPER BOUND(ID) transformation)

(46) Obligation:

(47) ResultPropagationProof (UPPER BOUND(ID) transformation)

(48) Obligation:

(49) IntTrsBoundProof (UPPER BOUND(ID) transformation)

(50) Obligation:

(51) IntTrsBoundProof (UPPER BOUND(ID) transformation)

(52) Obligation:

(53) ResultPropagationProof (UPPER BOUND(ID) transformation)

(54) Obligation:

(55) IntTrsBoundProof (UPPER BOUND(ID) transformation)

(56) Obligation:

(57) IntTrsBoundProof (UPPER BOUND(ID) transformation)

(58) Obligation:

(59) FinalProof (EQUIVALENT transformation)

(60) BOUNDS(1, n^1)